Realisierung mit Constraints

Inferenz für Aussagen der Form E $\vdash$ X : (T, C)

• E: Umgebung (Name → Typ)
• X: Ausdruck (Exp)
• T: Typ
• C: Menge von Typ-Constraints

wobei

• Menge der Typen T erweitert um Variablen
• Constraint: Paar von Typen (T₁, T₂)
• Lösung eines Constraints: Substitution σ mit T₁σ = T₂σ