System F

• einfach getypter Lambda-Kalkül:

  A $\Rightarrow$ x | AA | $\lambda$x : T.A

  T $\Rightarrow$ $\mathbb {N}$ | T$\to$T

  Variable x, Type T, Term A

• polymorph getypter Lambda-Kalkül (System F) (Jean-Yves Girard, John C. Reynolds)

  A $\Rightarrow$ ...$\Lambda$X.A | A[T],      T $\Rightarrow$ ...X | $\forall$X.T

  Typvariable X

• Hindley-Milner (benutzt in Standard-Haskell): Typ-Forall nur außen erlaubt