Merge branch 'master' of github.com:dhil/phd-dissertation

macros.tex

@@ -7,6 +7,7 @@
 \newcommand{\BCalcRec}{\ensuremath{\lambda_{\mathsf{b}+\mathsf{rec}}}\xspace}
 \newcommand{\HCalc}{\ensuremath{\lambda_{\mathsf{h}}}\xspace}
 \newcommand{\EffCalc}{\ensuremath{\lambda_{\mathsf{eff}}}\xspace}
+\newcommand{\UCalc}{\ensuremath{\lambda_{\mathsf{u}}}\xspace}
 
 %%
 %% Calculi terms and types type-setting.
@@ -104,6 +105,7 @@
 \newcommand{\rulelabel}[2]{\ensuremath{\mathsf{#1\textrm{-}#2}}}
 \newcommand{\klab}[1]{\rulelabel{K}{#1}}
 \newcommand{\semlab}[1]{\rulelabel{S}{#1}}
+\newcommand{\usemlab}[1]{\rulelabel{U}{#1}}
 \newcommand{\tylab}[1]{\rulelabel{T}{#1}}
 \newcommand{\mlab}[1]{\rulelabel{M}{#1}}
 \newcommand{\siglab}[1]{\rulelabel{Sig}{#1}}
@@ -114,6 +116,8 @@
 %%
 \newcommand{\CatName}[1]{\textrm{#1}}
 \newcommand{\CompCat}{\CatName{Comp}}
+\newcommand{\UCompCat}{\CatName{UComp}}
+\newcommand{\UValCat}{\CatName{UVal}}
 \newcommand{\ValCat}{\CatName{Val}}
 \newcommand{\VarCat}{\CatName{Var}}
 \newcommand{\ValTypeCat}{\CatName{VType}}
@@ -130,6 +134,7 @@
 \newcommand{\TyEnvCat}{\CatName{TyEnv}}
 \newcommand{\KindEnvCat}{\CatName{KindEnv}}
 \newcommand{\EvalCat}{\CatName{Cont}}
+\newcommand{\UEvalCat}{\CatName{UCont}}
 \newcommand{\HandlerCat}{\CatName{HDef}}
 
 %%
@@ -166,4 +171,76 @@
 %%
 %% Partiality
 %%
-\newcommand{\pto}[0]{\ensuremath{\rightharpoonup}}
+\newcommand{\pto}[0]{\ensuremath{\rightharpoonup}}
+
+%%
+%% Lists
+%%
+\newcommand{\nil}{\ensuremath{[]}}
+\newcommand{\cons}{\ensuremath{::}}
+
+\newcommand{\concat}{\mathbin{+\!\!+}}
+\newcommand{\revconcat}{\mathbin{\widehat{\concat}}}
+
+%%
+%% CPS notation
+%%
+% static / dynamic stuff
+\newcommand{\scol}[1]{{\color{blue}#1}}
+\newcommand{\dcol}[1]{{\color{red}#1}}
+
+\newcommand{\static}[1]{\scol{\overline{#1}}}
+\newcommand{\dynamic}[1]{\dcol{\underline{#1}}}
+\newcommand{\nary}[1]{\overline{#1}}
+
+\newcommand{\slam}{\static{\lambda}}
+\newcommand{\dlam}{\dynamic{\lambda}}
+\newcommand{\sapp}{\mathbin{\static{@}}}
+\newcommand{\dapp}{\mathbin{\dynamic{@}}}
+
+\newcommand{\reify}{\mathord{\downarrow}}
+\newcommand{\reflect}{\mathord{\uparrow}}
+
+\newcommand{\scons}{\mathbin{\static{\cons}}}
+\newcommand{\dcons}{\mathbin{\dynamic{\cons}}}
+
+\newcommand{\snil}{\static{\nil}}
+\newcommand{\dnil}{\dynamic{\nil}}
+
+\newcommand{\sRecord}[1]{\static{\langle}#1\static{\rangle}}
+\newcommand{\dRecord}[1]{\dynamic{\langle}#1\dynamic{\rangle}}
+
+%\newcommand{\sP}{\mathcal{P}}
+\newcommand{\sQ}{\mathcal{Q}}
+\newcommand{\sV}{\mathcal{V}}
+\newcommand{\sW}{\mathcal{W}}
+
+\newcommand{\sM}{\mathcal{M}}
+\renewcommand{\snil}{\reflect \dnil}
+
+\newcommand{\cps}[1]{\ensuremath{\llbracket #1 \rrbracket}}
+\newcommand{\pcps}[1]{\top\cps{#1}}
+
+\newcommand{\hforward}{M_{\textrm{forward}}}
+\newcommand{\hid}{V_{\textrm{id}}}
+
+%%% Continuation names
+%%% The following set of macros are a bit more consistent with those
+%%% currently used by the abstract machine, and don't use the plural
+%%% convention of functional programming.
+
+% dynamic
+\newcommand{\dlf}{f}    % let frames
+\newcommand{\dlk}{s}    % let continuations
+\newcommand{\dhf}{q}    % handler frames
+\newcommand{\dhk}{k}    % handler continuations
+\newcommand{\dhkr}{rk}  % reverse handler continuations
+
+% static
+\newcommand{\slf}{\phi}    % let frames
+\newcommand{\slk}{\sigma}  % let continuations
+\newcommand{\shf}{\theta}  % handler frames
+\newcommand{\shk}{\kappa}  % handler continuations
+
+\newcommand{\sP}{\mathcal{P}}
+\newcommand{\VS}{VS}

thesis.tex

@@ -1890,7 +1890,418 @@ getting stuck on an unhandled operation.
 
 \part{Implementation}
 
-\chapter{Continuation passing styles}
+\chapter{Continuation-passing styles}
+\label{ch:cps}
+
+Continuation-passing style (CPS) is a \emph{canonical} program
+notation that makes every facet of control flow and data flow
+explicit. In CPS every function takes an additional function-argument
+called the \emph{continuation}, which represents the next computation
+in evaluation position. CPS is canonical in the sense that is
+definable in pure $\lambda$-calculus without any primitives. As an
+informal illustration of CPS consider again the rudimentary factorial
+function from Section~\ref{sec:tracking-div}.
+%
+\[
+  \bl
+    \dec{fac} : \Int \to \Int\\
+    \dec{fac} \defas \Rec\;f~n.
+       \ba[t]{@{}l}
+         \Let\;is\_zero \revto n = 0\;\In\\
+         \If\;is\_zero\;\Then\; \Return\;1\\
+         \Else\;\ba[t]{@{~}l}
+                   \Let\; n' \revto n - 1 \;\In\\
+                   \Let\; m \revto f~n' \;\In\\
+                   n * m
+                 \ea
+       \ea
+  \el
+\]
+%
+The above implementation of the function $\dec{fac}$ is given in
+direct-style fine-grain call-by-value. In CPS notation the
+implementation of this function changes as follows.
+%
+\[
+  \bl
+  \dec{fac}_{\dec{cps}} : \Int \to (\Int \to \alpha) \to \alpha\\
+  \dec{fac}_{\dec{cps}} \defas \lambda n.\lambda k.
+     =_{\dec{cps}}~n~0~
+       (\ba[t]{@{~}l}
+          \lambda is\_zero.\\
+          \quad\ba[t]{@{~}l}
+          \If\;is\_zero\;\Then\; k~1\\
+          \Else\;
+          -_{\dec{cps}}~n~1~
+            (\lambda n'.
+               \dec{fac}_{\dec{cps}}~n'~
+                  (\lambda m. *_{\dec{cps}}~n~m~
+                  (\lambda res. k~res))))
+          \ea
+        \ea
+  \el
+\]
+%
+\dhil{Adjust the example to avoid stepping into the margin.}
+%
+There are several worthwhile observations to make about the
+differences between the two implementations $\dec{fac}$ and
+$\dec{fac}_{\dec{cps}}$.
+%
+Firstly note that their type signatures differ. The CPS version has an
+additional formal parameter of type $\Int \to \alpha$ which is the
+continuation. By convention the continuation parameter is named $k$ in
+the implementation. The continuation captures the remainder of
+computation that ultimately produces a result of type $\alpha$, or put
+differently: it determines what to do with the result returned by an
+invocation of $\dec{fac}$. Semantically the continuation corresponds
+to the surrounding evaluation
+context.% , thus with a bit of hand-waving
+% we can say that for $\EC[\dec{fac}~2]$ the entire evaluation $\EC$
+% would be passed as the continuation argument to the CPS version:
+% $\dec{fac}_{\dec{cps}}~2~\EC$.
+%
+Secondly note that every $\Let$-binding in $\dec{fac}$ has become a
+function application in $\dec{fac}_{\dec{cps}}$. The functions
+$=_{\dec{cps}}$, $-_{\dec{cps}}$, and $*_{\dec{cps}}$ denote the CPS
+versions of equality testing, subtraction, and multiplication
+respectively. Moreover, the explicit $\Return~1$ in the true branch
+has been turned into an application of continuation $k$, and the
+implicit return $n*m$ in the $\Else$-branch has been turned into an
+explicit application of the continuation.
+%
+Thirdly note every function application is in tail position. This is a
+characteristic property of CPS that makes CPS feasible as a practical
+implementation strategy since programs in CPS notation does not
+consume stack space.
+\dhil{The focus of the introduction should arguably not be to explain CPS.}
+\dhil{Justify CPS as an implementation technique}
+\dhil{Give a side-by-side reduction example of $\dec{fac}$ and $\dec{fac}_{\dec{cps}}$.}
+
+
+\section{Target calculus}
+\label{sec:target-cps}
+
+The syntax, semantics, and syntactic sugar for the target calculus
+$\UCalc$ is given in Figure~\ref{fig:cps-cbv-target}. The calculus
+largely amounts to an untyped variation of $\BCalcRec$, specifically
+we retain the syntactic distinction between values ($V$) and
+computations ($M$).
+%
+The values ($V$) comprise lambda abstractions ($\lambda x.M$),
+recursive functions ($\Rec\,g\,x.M$), empty tuples ($\Record{}$),
+pairs ($\Record{V,W}$), and first-class labels ($\ell$).
+%
+Computations ($M$) comprise values ($V$), applications ($M~V$), pair
+elimination ($\Let\; \Record{x, y} = V \;\In\; N$), label elimination
+($\Case\; V \;\{\ell \mapsto M; x \mapsto N\}$), and explicit marking
+of unreachable code ($\Absurd$). A key difference from $\BCalcRec$ is
+that the function position of an application is allowed to be a
+computation (i.e., the application form is $M~W$ rather than
+$V~W$). Later, when we refine the initial CPS translation we will be
+able to rule out this relaxation.
+
+We give a standard small-step evaluation context-based reduction
+semantics. Evaluation contexts comprise the empty context and function
+application.
+
+To make the notation more lightweight, we define syntactic sugar for
+variant values, record values, list values, let binding, variant
+eliminators, and record eliminators. We use pattern matching syntax
+for deconstructing variants, records, and lists. For desugaring
+records, we assume a failure constant $\ell_\bot$ (e.g. a divergent
+term) to cope with the case of pattern matching failure.
+
+\begin{figure}
+  \flushleft
+  \textbf{Syntax}
+  \begin{syntax}
+    \slab{Values}  &V, W \in \UValCat &::= &  x \mid \lambda x.M \mid \Rec\,g\,x.M \mid \Record{} \mid \Record{V, W} \mid \ell
+    \smallskip \\
+    \slab{Computations}  &M,N \in \UCompCat  &::= & V \mid M\,W \mid \Let\; \Record{x,y} = V \; \In \; N\\
+                         &     &\mid& \Case\; V\, \{\ell \mapsto M; y \mapsto N\} \mid \Absurd\,V
+    % &    &\mid& \Vmap\;(x.M)\;V \\
+    \smallskip \\
+    \slab{Evaluation contexts} &\EC \in \UEvalCat &::= & [~] \mid \EC\;W \\ %\mid \Let\; x \revto \EC \;\In\; N \\
+  \end{syntax}
+
+  \textbf{Reductions}
+  \begin{reductions}
+    \usemlab{App}   & (\lambda x . \, M) V &\reducesto& M[V/x] \\
+    \usemlab{Rec}   & (\Rec\,g\,x.M) V     &\reducesto& M[\Rec\,g\,x.M/g,V/x]\\
+    \usemlab{Split} & \Let \; \Record{x,y} = \Record{V,W} \; \In \; N &\reducesto& N[V/x,W/y] \\
+    \usemlab{Case_1} &
+    \Case \; \ell \; \{ \ell \mapsto M; y \mapsto N\} &\reducesto& M \\
+    \usemlab{Case_2} &
+    \Case \; \ell \; \{ \ell' \mapsto M; y \mapsto N\} &\reducesto& N[\ell/y], \hfill\quad \text{if } \ell \neq \ell' \\
+    % \usemlab{VMap}      & \Vmap\, (x.M) \,(\ell\, V) &\reducesto& \ell\, M[V/x] \\
+    \usemlab{Lift} &
+    \EC[M] &\reducesto& \EC[N], \hfill \text{if } M \reducesto N \\
+  \end{reductions}
+
+  \textbf{Syntactic sugar}
+\[
+    \begin{eqs}
+      \Let\;x=V\;\In\;N &\equiv & N[V/x]\\
+      \ell \; V & \equiv & \Record{\ell; V}\\
+      \Record{} & \equiv & \ell_{\Record{}} \\
+      \Record{\ell = V; W} & \equiv & \Record{\ell, \Record{V, W}}\\
+      \nil &\equiv & \ell_{\nil} \\
+      V \cons W & \equiv & \Record{\ell_{\cons}, \Record{V, W}}\\
+      \Case\;V\;\{\ell\;x \mapsto M; y \mapsto N \} &\equiv&
+        \ba[t]{@{~}l}
+            \Let\;y = V\;\In\; \Let\;\Record{z,x} = y\;\In \\
+            \Case\; z\;\{ \ell \mapsto M; z' \mapsto N \}
+        \ea\\
+      \Let\; \Record{\ell=x;y} = V\;\In\;N &\equiv&
+        \ba[t]{@{~}l}
+            \Let\; \Record{z,z'} = V\;\In\;\Let\; \Record{x,y} = z'\;\In \\
+            \Case\;z\;\{\ell \mapsto N; z'' \mapsto \ell_\bot \}
+            \ea
+    \end{eqs}
+\]
+
+\caption{Untyped target calculus for the CPS translations.}
+\label{fig:cps-cbv-target}
+\end{figure}
+
+\section{CPS transform for fine-grain call-by-value}
+\label{sec:cps-cbv}
+
+We start by giving a CPS translation of $\BCalcRec$ in
+Figure~\ref{fig:cps-cbv}. Fine-grain call-by-value admits a
+particularly simple CPS translation due to the separation of values
+and computations. All constructs from the source language are
+translated homomorphically into the target language $\UCalc$, except
+for $\Return$ and $\Let$ (and type abstraction because the translation
+performs type erasure). Lifting a value $V$ to a computation
+$\Return~V$ is interpreted by passing the value to the current
+continuation $k$. Sequencing computations with $\Let$ is translated by
+applying the translation of $M$ to the translation of the continuation
+$N$, which is ultimately applied to the current continuation $k$. In
+addition, we explicitly $\eta$-expand the translation of a type
+abstraction in order to ensure that value terms in the source calculus
+translate to value terms in the target.
+
+\begin{figure}
+\flushleft
+\textbf{Values} \\
+\[
+\bl
+
+\begin{eqs}
+  \cps{-}                  &:& \ValCat \to \UValCat\\
+\cps{x}                    &=& x \\
+\cps{\lambda x.M}          &=& \lambda x.\cps{M} \\
+\cps{\Lambda \alpha.M}     &=& \lambda k.\cps{M}~k \\
+\cps{\Rec\,g\,x.M}         &=& \Rec\,g\,x.\cps{M}\\
+\cps{\Record{}}            &=& \Record{} \\
+\cps{\Record{\ell = V; W}} &=& \Record{\ell = \cps{V}; \cps{W}} \\
+\cps{\ell~V}               &=& \ell~\cps{V} \\
+\end{eqs}
+\el
+\]
+\textbf{Computations}
+\[
+\bl
+\begin{eqs}
+\cps{-}                                         &:& \CompCat \to \UCompCat\\
+\cps{V\,W}                                      &=& \cps{V}\,\cps{W} \\
+\cps{V\,T}                                      &=& \cps{V} \\
+\cps{\Let\; \Record{\ell=x;y} = V \; \In \; N}  &=& \Let\; \Record{\ell=x;y} = \cps{V} \; \In \; \cps{N} \\
+\cps{\Case~V~\{\ell~x \mapsto M; y \mapsto N\}} &=&
+  \Case~\cps{V}~\{\ell~x \mapsto \cps{M}; y \mapsto \cps{N}\} \\
+\cps{\Absurd~V}                                 &=& \Absurd~\cps{V} \\
+\cps{\Return~V}                                 &=& \lambda k.k~\cps{V} \\
+\cps{\Let~x \revto M~\In~N}                     &=& \lambda k.\cps{M}(\lambda x.\cps{N}k) \\
+\end{eqs}
+\el
+\]
+\caption{First-order CPS translation of fine-grain call-by-value.}
+\label{fig:cps-cbv}
+\end{figure}
+
+\subsection{First-order CPS translations of effect handlers}
+\label{sec:fo-cps}
+
+The translation of a computation term by the basic CPS translation in
+Section~\ref{sec:cps-cbv} takes a single continuation parameter that
+represents the context.
+%
+In the presence of effect handlers in the source language, it becomes
+necessary to keep track of two kinds of contexts in which each
+computation executes: a \emph{pure context} that tracks the state of
+pure computation in the scope of the current handler, and an
+\emph{effect context} that describes how to handle operations in the
+scope of the current handler.
+%
+Correspondingly, we have both \emph{pure continuations} ($k$) and
+\emph{effect continuations} ($h$).
+%
+As handlers can be nested, each computation executes in the context of
+a \emph{stack} of pairs of pure and effect continuations.
+
+On entry into a handler, the pure continuation is initialised to a
+representation of the return clause and the effect continuation to a
+representation of the operation clauses. As pure computation proceeds,
+the pure continuation may grow, for example when executing a
+$\Let$. If an operation is encountered then the effect continuation is
+invoked.
+%
+The current continuation pair ($k$, $h$) is packaged up as a
+\emph{resumption} and passed to the current handler along with the
+operation and its argument. The effect continuation then either
+handles the operation, invoking the resumption as appropriate, or
+forwards the operation to an outer handler. In the latter case, the
+resumption is modified to ensure that the context of the original
+operation invocation can be reinstated when the resumption is invoked.
+%
+
+\subsubsection{Curried translation}
+\label{sec:first-order-curried-cps}
+
+We first consider a curried CPS translation that builds the
+translation of Figure~\ref{fig:cps-cbv}. The extension to operations
+and handlers is localised to the additional features because currying
+conveniently lets us get away with a shift in interpretation: rather
+than accepting a single continuation, translated computation terms now
+accept an arbitrary even number of arguments representing the stack of
+pure and effect continuations. Thus, we can conservatively extend the
+translation in Figure~\ref{fig:cps-cbv} to cover $\HCalc$, where we
+imagine there being some number of extra continuation arguments that
+have been $\eta$-reduced.  The translation of operations and handlers
+is as follows.
+%
+\begin{equations}
+\cps{\Do\;\ell\;V} &=& \lambda k.\lambda h.h~\Record{\ell,\Record{\cps{V}, \lambda x.k~x~h}} \\
+\cps{\Handle \; M \; \With \; H} &=& \cps{M}~\cps{\hret}~\cps{\hops}, ~\text{where} \smallskip\\
+\multicolumn{3}{@{}l@{}}{
+\begin{eqs}
+\qquad
+\cps{\{ \Return \; x \mapsto N \}} &=& \lambda x . \lambda h . \cps{N} \\
+\cps{\{ \ell~p~r \mapsto N_\ell \}_{\ell \in \mathcal{L}}}
+&=&
+\lambda \Record{z,\Record{p,r}}. \Case~z~
+           \{ (\ell \mapsto \cps{N_\ell})_{\ell \in \mathcal{L}}; y \mapsto \hforward(y,p,r) \} \\
+           \hforward(y,p,r) &=& \lambda k. \lambda h. h\,\Record{y,\Record{p, \lambda x.\,r\,x\,k\,h}}
+\end{eqs}
+}
+\end{equations}
+%
+The translation of $\Do\;\ell\;V$ abstracts over the current pure
+($k$) and effect ($h$) continuations passing an encoding of the
+operation into the latter. The operation is encoded as a triple
+consisting of the name $\ell$, parameter $\cps{V}$, and resumption
+$\lambda x.k~x~h$, which passes the same effect continuation $h$ to
+ensure deep handler semantics.
+
+The translation of $\Handle~M~\With~H$ invokes the translation of $M$
+with new pure and effect continuations for the return and operation
+clauses of $H$.
+%
+The translation of a return clause is a term which garbage collects
+the current effect continuation $h$.
+%
+The translation of a set of operation clauses is a function which
+dispatches on encoded operations, and in the default case forwards to
+an outer handler.
+%
+In the forwarding case, the resumption is extended by the parent
+continuation pair in order to reinstate the handler stack, thereby
+ensuring subsequent invocations of the same operation are handled
+uniformly.
+
+The translation of complete programs feeds the translated term the
+identity pure continuation (which discards its handler argument), and
+an effect continuation that is never intended to be called.
+%
+\begin{equations}
+\pcps{M} &=& \cps{M}~(\lambda x.\lambda h.x)~(\lambda \Record{z,\_}.\Absurd~z) \\
+\end{equations}
+%
+Conceptually, this translation encloses the translated program in a
+top-level handler with an empty collection of operation clauses and an
+identity return clause.
+
+% There are three shortcomings of this initial translation that we
+% address below.
+
+% \begin{itemize}
+% \item First, it is not \emph{properly tail-recursive}~\citep{DanvyF92,
+%   Steele78} due to the curried representation of the continuation
+%   stack, as a result the image of the translation is not stackless,
+%   which makes it problematic to implement using a trampoline in, say,
+%   JavaScript. (Properly tail-recursion CPS translations ensure that
+%   all calls to functions and continuations are in tail position, hence
+%   there is no need to maintain a stack.) We rectify this issue with an
+%   explicit list representation in the next subsection.
+
+% \item Second, it yields administrative redexes (redexes that could be
+%   reduced statically). We will rectify this with a higher-order
+%   one-pass translation in
+%   Section~\ref{sec:higher-order-uncurried-cps}.
+
+% \item Third, this translation cannot cope with shallow handlers. The
+%   pure continuations $k$ are abstract and include the return clause of
+%   the corresponding handler. Shallow handlers require that the return
+%   clause of a handler is discarded when one of its operations is
+%   invoked. We will fix this in Section~\ref{sec:pure-as-stack}, where we
+%   will represent pure continuations as explicit stacks.
+% \end{itemize}
+
+% To illustrate the first two issues, consider the following example:
+% \begin{equations}
+% \pcps{\Return\;\Record{}}
+%               &=& (\lambda k.k\,\Record{})\,(\lambda x.\lambda h.x)\,(\lambda \Record{z,\_}.\Absurd\,z)  \\
+%      &\reducesto& ((\lambda x.\lambda h.x)\,\Record{})\,(\lambda \Record{z,\_}.\Absurd\,z)\\
+%      &\reducesto& (\lambda h.\Record{})\,(\lambda \Record{z,\_}.\Absurd\,z)\\
+%      &\reducesto& \Record{} \\
+% \end{equations}
+% The first reduction is administrative: it has nothing to do with the
+% dynamic semantics of the original term and there is no reason not to
+% eliminate it statically. The second and third reductions simulate
+% handling $\Return\;\Record{}$ at the top level. The second reduction
+% partially applies $\lambda x.\lambda h.x$ to $\Record{}$, which must
+% return a value so that the third reduction can be applied: evaluation
+% is not tail-recursive.
+% %
+% The lack of tail-recursion is also apparent in our relaxation of
+% fine-grain call-by-value in Figure~\ref{fig:cps-cbv-target}: the
+% function position of an application can be a computation, and the
+% calculus makes use of evaluation contexts.
+
+% \paragraph*{Remark}
+% We originally derived this curried CPS translation for effect handlers
+% by composing \citeauthor{ForsterKLP17}'s translation from effect
+% handlers to delimited continuations~\citeyearpar{ForsterKLP17} with
+% \citeauthor{MaterzokB12}'s CPS translation for delimited
+% continuations~\citeyearpar{MaterzokB12}.
+
+% \medskip
+
+\dhil{Discuss deficiencies of the curried translation}
+\dhil{State simulation result}
+% Because of the administrative reductions, simulation is not on the
+% nose, but instead up to congruence.
+% %
+% For reduction in the untyped target calculus we write
+% $\reducesto_{\textrm{cong}}$ for the smallest relation containing
+% $\reducesto$ that is closed under the term formation constructs.
+% %
+% \begin{theorem}[Simulation]
+%   \label{thm:fo-simulation}
+%   If $M \reducesto N$ then $\pcps{M} \reducesto_{\textrm{cong}}^+
+%   \pcps{N}$.
+% \end{theorem}
+
+% \begin{proof}
+% The result follows by composing a call-by-value variant of
+% \citeauthor{ForsterKLP17}'s translation from effect handlers to
+% delimited continuations~\citeyearpar{ForsterKLP17} with
+% \citeauthor{MaterzokB12}'s CPS translation for delimited
+% continuations~\citeyearpar{MaterzokB12}.
+% \end{proof}
+
 \chapter{Abstract machine semantics}
 
 \part{Expressiveness}