\begin{slide}{Typen und Terme}

  \begin{itemize}
  \item (Term abhängig von Term, Funktion auf Daten)
  \item Typ abhängig von Typ (Typkonstruktoren: Functor, Monad)
  \item Term abhängig von Typ (System F)
  \item Typ abhängig von Term (dependent Types: Coq, PVS, \dots)
  \end{itemize}
(der Lambda-Würfel, Barendregt 1991)
\url{http://www.cs.ru.nl/~henk/}


\end{slide}
