Properly tail-recursive CPS definition.

thesis.bib

@@ -579,6 +579,15 @@
   year      = {1992}
 }
 
+@phdthesis{Danvy06,
+  author = {Olivier Danvy},
+  school = {Aarhus University},
+  title = {An Analytical Approach to Programs as Data Objects},
+  type = {{DSc} thesis},
+  year = 2006,
+  address = {Aarhus, Denmark}
+}
+
 @book{Appel92,
   author    = {Andrew W. Appel},
   title     = {Compiling with Continuations},
@@ -874,7 +883,8 @@
   school = {Universit{\'e} Paris 7},
   title = {Interpr{\'e}tation fonctionnelle et {\'e}limination des coupures de l'arithm{\'e}tique d'ordre sup{\'e}rieur},
   type = {PhD thesis},
-  year = 1972
+  year = 1972,
+  address = {Paris, France}
 }
 
 @inproceedings{Reynolds74,

thesis.tex

@@ -24,6 +24,8 @@
 \usepackage[T1]{fontenc}      % Fixes issues with accented characters
 %\usepackage{libertine}
 %\usepackage{lmodern}
+%\usepackage{palatino}
+% \usepackage{newpxtext,newpxmath}
 \usepackage[activate=true,
     final,
     tracking=true,
@@ -2102,6 +2104,17 @@ not consume stack space.
 \dhil{Justify CPS as an implementation technique}
 \dhil{Give a side-by-side reduction example of $\dec{fac}$ and $\dec{fac}_{\dec{cps}}$.}
 \dhil{Define desirable properties of a CPS translation: properly tail-recursive, no static administrative redexes}
+%
+\begin{definition}[Properly tail-recursive~\cite{Danvy06}]
+ %
+  A CPS translation $\cps{-}$ is properly tail-recursive if the
+  continuation of every CPS transformed tail call $\cps{V\,W}$ within
+  $\cps{\lambda x.M}$ is $k$, where
+  \begin{equations}
+      \cps{\lambda x.M} &=& \lambda x.\lambda k.\cps{M}\\
+      \cps{V\,W} &=& \cps{V}\,\cps{W}\,k.
+    \end{equations}
+\end{definition}
 
 \section{Initial target calculus}
 \label{sec:target-cps}