\newcommand{\CPS}{\operatorname{CPS}}
\newcommand{\Eval}{\operatorname{Eval}}


\begin{slide}{Übung: Ergänzung CPS}

Gordon Plotkin: 
\emph{Call-by-name, call-by-value, and the Lambda calculus},
Theoretical Computer Science 1(2):125--159, 1975)
\url{http://dx.doi.org/10.1016/0304-3975(75)90017-1}
Transformation (Abschnitt 6):
\begin{itemize}\itemsep 0pt
\item Variable: $\CPS[x] = \lambda k.kx$
\item Abstraktion: $\CPS[\lambda x.M] = \lambda k.k(\lambda x.\CPS[M])$
\item Applikation: $\CPS[F A]=
  \lambda k.\CPS[F](\lambda f.\CPS[A] (\lambda a.f a k))$
\end{itemize}

Ausssage (S. 148, Thm. 6.2)
$\Psi(\Eval_{\text{by-value}}(M)) = \Eval_{\text{by-name}}(\CPS[M](\lambda x.x))$

wesentliche für Beweis ist Lemma 6.1
$\CPS[M](x:=\Psi(N)) = \CPS[M(x:=N)]$

\bigskip

Transformation erzeugt \glqq administrative Redexe\grqq,
verschiedene Strategien zu deren Vermeidung, vgl.

Zaynah Dargaye and Xavier Leroy. 
\emph{Mechanized verification of CPS transformations.} LPAR 2007
\url{http://cristal.inria.fr/~xleroy/bibrefs/Dargaye-Leroy-CPS.html}

zusammengefaßt in:
Martijn Vermaat: \emph{Verifying a CPS Transformation}
(Bachelor project, VU Amsterdam)
\url{http://www.cs.vu.nl/~mvermaat/files/vu/bachelor-project/slides.pdf}

in DCPL benutzt: Meta-Continuations
(entspricht ``smart application'' $@_{\beta}$ aus Dargaye/Leroy S. 5)

\end{slide}
