\begin{slide}{Regeln zur Typprüfung}

\dots bei geschachtelten Funktionsaufrufen

\begin{itemize}
\item Funktion $f$ hat Typ $A \to B$
\item Ausdruck $X$ hat Typ $A$
\item dann hat Ausdruck $f(X)$ den Typ $B$
\end{itemize}

Beispiel
\begin{verbatim}
String x = "foo"; String y = "bar";

Boolean.toString (x.length() < y.length()));
\end{verbatim}

\bigskip

(Curry-Howard-Isomorphie)

\end{slide}

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
