Inferenzsystem für Typen (Syntax)

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

  (in Umgebung E mathend000# hat Ausdruck X mathend000# den Typ T mathend000#)

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