Realisierung mit Constraints

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

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

wobei

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