Inferenzsystem für Typen (Syntax)

• Grundbereich: Aussagen der Form E $\vdash$ X : T

  (in Umgebung E hat Ausdruck X den Typ T)

• Menge der Typen:
  • primitiv: Int, Bool
  • zusammengesetzt:
    • Funktion T₁→T₂
    • Verweistyp RefT
    • Tupel (T₁,…, T_n), einschl. n = 0
• Umgebung bildet Namen auf Typen ab