Inferenzsystem für Typen (Semantik)

• Axiome f. Literale: E $\vdash$ Zahl-Literal : Int mathend000#, ...
• Regel für prim. Operationen: $${\frac{{E\vdash X : \text{Int},E\vdash Y : \text{Int}}}{{E \vdash (X+Y) : \text{Int}}}}$$ mathend000#, ...
• Abstraktion/Applikation: ...

• Binden/Benutzen von Bindungen: ...

hierbei (vorläufige) Design-Entscheidungen:

• Typ eines Ausdrucks wird inferiert
• Typ eines Bezeichners wird ...
  • in Abstraktion: deklariert
  • in Let: inferiert