\begin{slide}{System F}

  \begin{itemize}
  \item 
einfach getypter Lambda-Kalkül:

$A \Rightarrow x \mid A A \mid \lambda x:T . A $ 

$T \Rightarrow \NN \mid T \to T$

Variable $x$, Type $T$, Term $A$
\item
  polymorph getypter Lambda-Kalkül (System $F$)
(Jean-Yves Girard, John C. Reynolds)


$A \Rightarrow \dots \Lambda X.A \mid A[T]$, 
\quad $T \Rightarrow \dots X \mid \forall X.T$

Typvariable $X$
\item
  Hindley-Milner (benutzt in Standard-Haskell): Typ-Forall nur außen erlaubt

  \end{itemize}

\end{slide}
