Applikation und Abstraktion

• Applikation:
  $${\frac{{E\vdash F : T_1 \to T_2, \quad E \vdash A : T_1}}{{E \vdash (F A) : T_2}}}$$

  vergleiche mit modus ponens

• Abstraktion (mit deklariertem Typ der Variablen)
  $${\frac{{E[v:=T_1] \vdash X : T_2}}{{E\vdash (\lambda (v :: T_1) X) : T_1 \to T_2}}}$$