\begin{slide}{Typen und Daten}

  \begin{itemize}\parskip 1pt
  \item bisher: Funktionen von Daten nach Daten
    
    \verb|\ (x :: Int) -> x + 1|
  \item heute: Funktionen von Typ nach Daten

    \verb|\ (t :: Type) -> \ (x :: t) -> x|
  \item Funktionen von Typ nach Typ (ML, Haskell, Java, C\#)

    \verb|\ (t :: Type) -> List t|
  \item Funktionen von Daten nach Typ 
    (\emph{dependent types})

    \verb|\ (t :: Typ) (n :: Int) -> Array t n|

    Sprachen: Cayenne, Coq, Agda

    Eigenschaften: Typkorrektheit i. A. nicht entscheidbar,

    d. h. Programmierer muß Beweis hinschreiben.

  \end{itemize}




\end{slide}
