Begin paragraph on CPS

macros.tex

@@ -427,8 +427,8 @@
 \newcommand{\Set}{\keyw{set}}
 \newcommand{\newPrompt}{\keyw{newPrompt}}
 \newcommand{\Callcc}{\keyw{callcc}}
-\newcommand{\Callcomc}{\ensuremath{\keyw{callcc}^\ast}}
-\newcommand{\textCallcomc}{callcc$^\ast$}
+\newcommand{\Callcomc}{\ensuremath{\keyw{callcomp}}}
+\newcommand{\textCallcomc}{callcomp}
 \newcommand{\Throw}{\keyw{throw}}
 \newcommand{\Continue}{\keyw{resume}}
 \newcommand{\Catch}{\keyw{catch}}

thesis.bib

@@ -51,24 +51,27 @@
   year      = {2017}
 }
 
-# Efficient one-shot continuations
+# Segmented stacks
+@inproceedings{HiebDB90,
+  author    = {Robert Hieb and
+               R. Kent Dybvig and
+               Carl Bruggeman},
+  title     = {Representing Control in the Presence of First-Class Continuations},
+  booktitle = {{PLDI}},
+  pages     = {66--77},
+  publisher = {{ACM}},
+  year      = {1990}
+}
+
 @inproceedings{BruggemanWD96,
   author    = {Carl Bruggeman and
                Oscar Waddell and
                R. Kent Dybvig},
-  editor    = {Charles N. Fischer},
   title     = {Representing Control in the Presence of One-Shot Continuations},
-  booktitle = {Proceedings of the {ACM} SIGPLAN'96 Conference on Programming Language
-               Design and Implementation (PLDI), Philadephia, Pennsylvania, May 21-24,
-               1996},
+  booktitle = {{PLDI}},
   pages     = {99--107},
   publisher = {{ACM}},
-  year      = {1996},
-  OPTurl       = {http://doi.acm.org/10.1145/231379.231395},
-  OPTdoi       = {10.1145/231379.231395},
-  timestamp = {Mon, 21 May 2012 16:19:53 +0200},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/pldi/BruggemanWD96},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
+  year      = {1996}
 }
 
 # Programming with continuations
@@ -158,21 +161,13 @@
 }
 
 # Other algebraic effects and handlers
-@InProceedings{Lindley14,
+@inproceedings{Lindley14,
   author    = {Sam Lindley},
-  editor    = {Jos{\'{e}} Pedro Magalh{\~{a}}es and
-               Tiark Rompf},
   title     = {Algebraic effects and effect handlers for idioms and arrows},
-  booktitle = {Proceedings of the 10th {ACM} {SIGPLAN} workshop on Generic programming,
-               {WGP} 2014, Gothenburg, Sweden, August 31, 2014},
+  booktitle = {WGP@ICFP},
   pages     = {47--58},
   publisher = {{ACM}},
-  year      = {2014},
-  OPTurl       = {http://doi.acm.org/10.1145/2633628.2633636},
-  OPTdoi       = {10.1145/2633628.2633636},
-  timestamp = {Thu, 25 Jun 2015 13:50:37 +0200},
-  biburl    = {http://dblp.uni-trier.de/rec/bib/conf/icfp/Lindley14},
-  bibsource = {dblp computer science bibliography, http://dblp.org}
+  year      = {2014}
 }
 
 @article{Pretnar15,
@@ -1463,6 +1458,20 @@
   month      = aug
 }
 
+# callcomp
+@inproceedings{FlattYFF07,
+  author    = {Matthew Flatt and
+               Gang Yu and
+               Robert Bruce Findler and
+               Matthias Felleisen},
+  title     = {Adding delimited and composable control to a production programming
+               environment},
+  booktitle = {{ICFP}},
+  pages     = {165--176},
+  publisher = {{ACM}},
+  year      = {2007}
+}
+
 # Constraining call/cc
 @inproceedings{FriedmanH85,
   author    = {Daniel P. Friedman and
@@ -1819,6 +1828,17 @@
   address = {Scotland, {UK}}
 }
 
+@article{DybvigH89,
+  author    = {R. Kent Dybvig and
+               Robert Hieb},
+  title     = {Engines From Continuations},
+  journal   = {Comput. Lang.},
+  volume    = {14},
+  number    = {2},
+  pages     = {109--123},
+  year      = {1989}
+}
+
 @inproceedings{HiebD90,
   author    = {Robert Hieb and
                R. Kent Dybvig},
@@ -2267,3 +2287,125 @@
   year      = {1994}
 }
 
+# Differentiable programming with delimited continuations
+@article{WangZDWER19,
+  author    = {Fei Wang and
+               Daniel Zheng and
+               James M. Decker and
+               Xilun Wu and
+               Gr{\'{e}}gory M. Essertel and
+               Tiark Rompf},
+  title     = {Demystifying differentiable programming: shift/reset the penultimate
+               backpropagator},
+  journal   = {Proc. {ACM} Program. Lang.},
+  volume    = {3},
+  number    = {{ICFP}},
+  pages     = {96:1--96:31},
+  year      = {2019}
+}
+
+# Probabilistic programming with continuations
+@inproceedings{KiselyovS09,
+  author    = {Oleg Kiselyov and
+               Chung{-}chieh Shan},
+  title     = {Embedded Probabilistic Programming},
+  booktitle = {{DSL}},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {5658},
+  pages     = {360--384},
+  publisher = {Springer},
+  year      = {2009}
+}
+
+
+@InProceedings{GorinovaMH20,
+  title = {Automatic Reparameterisation of Probabilistic Programs},
+  author = {Maria I. Gorinova and Dave Moore and Matthew D. Hoffman},
+  booktitle = {{ICML}},
+  pages = {3648--3657},
+  year = {2020},
+  OPTeditor = {Hal Daumé III and Aarti Singh},
+  volume = {119},
+  OPTseries = {Proceedings of Machine Learning Research},
+  OPTaddress = {Virtual},
+  OPTmonth = {13--18 Jul},
+  publisher = {PMLR},
+  OPTpdf = {http://proceedings.mlr.press/v119/gorinova20a/gorinova20a.pdf},
+  OPTurl = {http://proceedings.mlr.press/v119/gorinova20a.html},
+}
+
+# Continuations in operating systems
+@inproceedings{KiselyovS07a,
+  author    = {Oleg Kiselyov and
+               Chung{-}chieh Shan},
+  title     = {Delimited Continuations in Operating Systems},
+  booktitle = {{CONTEXT}},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {4635},
+  pages     = {291--302},
+  publisher = {Springer},
+  year      = {2007}
+}
+
+# Web programming and continuations
+@article{Queinnec04,
+  author    = {Christian Queinnec},
+  title     = {Continuations and Web Servers},
+  journal   = {High. Order Symb. Comput.},
+  volume    = {17},
+  number    = {4},
+  pages     = {277--295},
+  year      = {2004}
+}
+
+# Erlang
+@book{ArmstrongVW93,
+  author    = {Joe Armstrong and
+               Robert Virding and
+               Mike Williams},
+  title     = {Concurrent programming in {ERLANG}},
+  publisher = {Prentice Hall},
+  year      = {1993}
+}
+
+# Asynchrony with effect handlers
+@inproceedings{Leijen17a,
+  author    = {Daan Leijen},
+  title     = {Structured asynchrony with algebraic effects},
+  booktitle = {TyDe@ICFP},
+  pages     = {16--29},
+  publisher = {{ACM}},
+  year      = {2017}
+}
+
+# Surveys of implementation strategies for continuations
+@inproceedings{ClingerHO88,
+  author    = {William D. Clinger and
+               Anne Hartheimer and
+               Eric Ost},
+  title     = {Implementation Strategies for Continuations},
+  booktitle = {{LISP} and Functional Programming},
+  pages     = {124--131},
+  publisher = {{ACM}},
+  year      = {1988}
+}
+
+@inproceedings{FarvardinR20,
+  author    = {Kavon Farvardin and
+               John H. Reppy},
+  title     = {From folklore to fact: comparing implementations of stacks and continuations},
+  booktitle = {{PLDI}},
+  pages     = {75--90},
+  publisher = {{ACM}},
+  year      = {2020}
+}
+
+# Non-contiguous stacks
+@inproceedings{Danvy87,
+  author    = {Olivier Danvy},
+  title     = {Memory allocation and higher-order functions},
+  booktitle = {{PLDI}},
+  pages     = {241--252},
+  publisher = {{ACM}},
+  year      = {1987}
+}

thesis.tex

@@ -568,42 +568,6 @@ the translation preserve typeability.
 \citet{Shan04} shows that dynamic delimited control and static
 delimited control is macro-expressible in an untyped setting.
 
-\paragraph{A language for understanding control}
-%
-To look at control we will a simply typed fine-grain call-by-value
-calculus. The calculus is essentially the same as the one used in
-Chapter~\ref{ch:handlers-efficiency}, except that here we will have an
-explicit invocation form for continuations. Although, in practice most
-systems disguise continuations as first-class functions, but for a
-theoretical examination it is convenient to treat them specially such
-that continuation invocation is a separate reduction rule from
-ordinary function application. Figure~\ref{fig:pcf-lang-control}
-depicts the syntax of types and terms in the calculus.
-%
-\begin{figure}
-  \centering
-\begin{syntax}
-  \slab{Types}        & A,B &::=& \UnitType \mid \Zero \mid A \to B \mid A + B \mid A \times B \mid \Cont\,\Record{A;B} \smallskip\\
-  \slab{Values}       & V,W &::=& x \mid \lambda x^A.M \mid V + W \mid \Record{V;W} \mid \Unit \mid \cont_\EC\\
-  \slab{Computations} & M,N &::=& \Return\;V \mid \Let\;x \revto M \;\In\;N \mid \Let \Record{x;y} = V \;\In\; N \\
-                       &     &\mid& \Absurd^A\;V \mid V\,W \mid \Continue~V~W \smallskip\\
-  \slab{Evaluation\textrm{ }contexts} & \EC &::=& [\,] \mid \Let\;x \revto \EC \;\In\;N
-\end{syntax}
-\caption{Types and term syntax}\label{fig:pcf-lang-control}
-\end{figure}
-%
-The types are the standard simple types with the addition of the empty
-type $\Zero$ and the continuation object type $\Cont\,\Record{A;B}$,
-which is parameterised by an argument type and a result type,
-respectively. The static semantics is standard as well, except for the
-continuation invocation primitive $\Continue$.
-%
-\begin{mathpar}
-    \inferrule*
-    {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}}
-    {\typ{\Gamma}{\Continue~W~V : B}}
-\end{mathpar}
-
 \section{Classifying continuations}
 
 % \citeauthor{Reynolds93} has written a historical account of the
@@ -756,6 +720,42 @@ non-exhaustive list of first-class control operators.
 \end{table}
 %
 
+\paragraph{An optical device for control}
+%
+To look at control we will a simply typed fine-grain call-by-value
+calculus. The calculus is essentially the same as the one used in
+Chapter~\ref{ch:handlers-efficiency}, except that here we will have an
+explicit invocation form for continuations. Although, in practice most
+systems disguise continuations as first-class functions, but for a
+theoretical examination it is convenient to treat them specially such
+that continuation invocation is a separate reduction rule from
+ordinary function application. Figure~\ref{fig:pcf-lang-control}
+depicts the syntax of types and terms in the calculus.
+%
+\begin{figure}
+  \centering
+\begin{syntax}
+  \slab{Types}        & A,B &::=& \UnitType \mid \Zero \mid A \to B \mid A + B \mid A \times B \mid \Cont\,\Record{A;B} \smallskip\\
+  \slab{Values}       & V,W &::=& x \mid \lambda x^A.M \mid V + W \mid \Record{V;W} \mid \Unit \mid \cont_\EC\\
+  \slab{Computations} & M,N &::=& \Return\;V \mid \Let\;x \revto M \;\In\;N \mid \Let \Record{x;y} = V \;\In\; N \\
+                       &     &\mid& \Absurd^A\;V \mid V\,W \mid \Continue~V~W \smallskip\\
+  \slab{Evaluation\textrm{ }contexts} & \EC &::=& [\,] \mid \Let\;x \revto \EC \;\In\;N
+\end{syntax}
+\caption{Types and term syntax}\label{fig:pcf-lang-control}
+\end{figure}
+%
+The types are the standard simple types with the addition of the empty
+type $\Zero$ and the continuation object type $\Cont\,\Record{A;B}$,
+which is parameterised by an argument type and a result type,
+respectively. The static semantics is standard as well, except for the
+continuation invocation primitive $\Continue$.
+%
+\begin{mathpar}
+    \inferrule*
+    {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}}
+    {\typ{\Gamma}{\Continue~W~V : B}}
+\end{mathpar}
+
 \subsection{Undelimited control operators}
 %
 The early inventions of undelimited control operators were driven by
@@ -817,28 +817,34 @@ available for use within $N$. \citeauthor{Reynolds98a} recognised the
 power of this idiom and noted that it could be used to implement
 coroutines and backtracking~\cite{Reynolds98a}.
 %
-In our simply-typed setting it is not possible for the continuation to
-propagate outside its binding $\Escape$-expression as it would require
-the addition of either recursive types or some other escape hatch like
+\citeauthor{Reynolds98a} did not develop the static semantics for
+$\Escape$, however, it is worth noting that this idiom require
+recursive types to type check. Even in a language without recursive
+types, the continuation may propagate outside its binding
+$\Escape$-expression if the language provides an escape hatch such as
 mutable reference cells.
-%
+% In our simply-typed setting it is not possible for the continuation to
+% propagate outside its binding $\Escape$-expression as it would require
+% the addition of either recursive types or some other escape hatch like
+% mutable reference cells.
+% %
 
-The typing of $\Escape$ and $\Continue$ reflects that the captured
-continuation is abortive.
-%
-\begin{mathpar}
-  \inferrule*
-    {\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}}
-    {\typ{\Gamma}{\Escape\;k\;\In\;M : A}}
+% The typing of $\Escape$ and $\Continue$ reflects that the captured
+% continuation is abortive.
+% %
+% \begin{mathpar}
+%   \inferrule*
+%     {\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}}
+%     {\typ{\Gamma}{\Escape\;k\;\In\;M : A}}
 
-  % \inferrule*
-  %   {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;\Zero}}}
-  %   {\typ{\Gamma}{\Continue~W~V : \Zero}}
-\end{mathpar}
-%
-The return type of the continuation object can be taken as a telltale
-sign that an invocation of this object never returns, since there are
-no inhabitants of the empty type.
+%   % \inferrule*
+%   %   {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;\Zero}}}
+%   %   {\typ{\Gamma}{\Continue~W~V : \Zero}}
+% \end{mathpar}
+% %
+% The return type of the continuation object can be taken as a telltale
+% sign that an invocation of this object never returns, since there are
+% no inhabitants of the empty type.
 %
 An invocation of the continuation discards the invocation context and
 plugs the argument into the captured context.
@@ -869,18 +875,17 @@ with access to the current continuation. Thus it is same as
   M,N ::= \cdots \mid \Catch~k.M
 \]
 %
-Although, their syntax differ, their static and dynamic semantics are
-the same.
+Although, their syntax differ, their dynamic semantics are the same.
 %
-\begin{mathpar}
-  \inferrule*
-    {\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}}
-    {\typ{\Gamma}{\Catch~k.M : A}}
+% \begin{mathpar}
+%   \inferrule*
+%     {\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}}
+%     {\typ{\Gamma}{\Catch~k.M : A}}
 
-  % \inferrule*
-  %   {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}}
-  %   {\typ{\Gamma}{\Continue~W~V : B}}
-\end{mathpar}
+%   % \inferrule*
+%   %   {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}}
+%   %   {\typ{\Gamma}{\Continue~W~V : B}}
+% \end{mathpar}
 %
 \begin{reductions}
   \slab{Capture} &  \EC[\Catch~k.M] &\reducesto& \EC[M[\qq{\cont_{\EC}}/k]]\\
@@ -909,25 +914,26 @@ categories of values.
 The value $\Callcc$ is essentially a hard-wired function name. Being a
 value means that the operator itself is a first-class entity which
 entails it can be passed to functions, returned from functions, and
-stored in data structures.
+stored in data structures. Operationally, $\Callcc$ captures the
+current continuation and aborts it before applying it on its argument.
 %
-The typing rule for $\Callcc$ testifies to the fact that it is a
-particular higher-order function.
+% The typing rule for $\Callcc$ testifies to the fact that it is a
+% particular higher-order function.
 %
-\begin{mathpar}
-  \inferrule*
-    {~}
-    {\typ{\Gamma}{\Callcc : (\Cont\,\Record{A;\Zero} \to A) \to A}}
+% \begin{mathpar}
+%   \inferrule*
+%     {~}
+%     {\typ{\Gamma}{\Callcc : (\Cont\,\Record{A;\Zero} \to A) \to A}}
 
-  % \inferrule*
-  %   {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}}
-  %   {\typ{\Gamma}{\Continue~W~V : B}}
-\end{mathpar}
-%
-An invocation of $\Callcc$ returns a value of type $A$. This value can
-be produced in one of two ways, either the function argument returns
-normally or it applies the provided continuation object to a value
-that then becomes the result of $\Callcc$-application.
+%   % \inferrule*
+%   %   {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}}
+%   %   {\typ{\Gamma}{\Continue~W~V : B}}
+% \end{mathpar}
+% %
+% An invocation of $\Callcc$ returns a value of type $A$. This value can
+% be produced in one of two ways, either the function argument returns
+% normally or it applies the provided continuation object to a value
+% that then becomes the result of $\Callcc$-application.
 %
 \begin{reductions}
   \slab{Capture} &  \EC[\Callcc~V] &\reducesto& \EC[V~\qq{\cont_{\EC}}]\\
@@ -946,20 +952,21 @@ macro-expressible.
 \end{equations}
 
 \paragraph{Call-with-composable-continuation} A variation of callcc is
-call-with-composable-continuation, or as I call it \textCallcomc{}.
+call-with-composable-continuation, abbreviated \textCallcomc{}.
 %
 As the name suggests the captured continuation is composable rather
-than abortive.
+than abortive. It was introduced by \citet{FlattYFF07} in 2007, and
+and implemented in November 2006 according to the history log of
+Racket (Racket was then known as MzScheme, version
+360)~\cite{Flatt20}. The history log classifies it as a delimited
+control operator.
 %
-According to the history log of Racket it appeared in November 2006
-(Racket was then known as MzScheme, version 360)~\cite{Flatt20}. The
-history log classifies it as a delimited control operator. Truth to be
-told nowadays in Racket virtually all control operators are delimited,
-even callcc, because they are parameterised by an optional prompt
-tag. If the programmer does not supply a prompt tag at invocation time
-then the optional parameter assume the actual value of the top-level
-prompt, effectively making the extent of the captured continuation
-undelimited.
+Truth to be told nowadays in Racket virtually all control operators
+are delimited, even callcc, because they are parameterised by an
+optional prompt tag. If the programmer does not supply a prompt tag at
+invocation time then the optional parameter assume the actual value of
+the top-level prompt, effectively making the extent of the captured
+continuation undelimited.
 %
 In other words its default mode of operation is undelimited, hence the
 justification for categorising it as such.
@@ -971,30 +978,31 @@ Like $\Callcc$ this operator is a value.
   V,W \in \ValCat ::= \cdots \mid \Callcomc
 \]
 %
-Unlike $\Callcc$, the continuation returns, which the typing rule for
-$\Callcomc$ reflects.
-%
-\begin{mathpar}
-  \inferrule*
-    {~}
-    {\typ{\Gamma}{\Callcomc : (\Cont\,\Record{A;A} \to A) \to A}}
+% Unlike $\Callcc$, the continuation returns, which the typing rule for
+% $\Callcomc$ reflects.
+% %
+% \begin{mathpar}
+%   \inferrule*
+%     {~}
+%     {\typ{\Gamma}{\Callcomc : (\Cont\,\Record{A;A} \to A) \to A}}
 
-  \inferrule*
-    {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}}
-    {\typ{\Gamma}{\Continue~W~V : B}}
-\end{mathpar}
-%
-Both the domain and codomain of the continuation are the same as the
-body type of function argument. The capture rule for $\Callcomc$ is
-identical to the rule for $\Callcomc$, but the resume rule is
-different.
+%   \inferrule*
+%     {\typ{\Gamma}{V : A} \\ \typ{\Gamma}{W : \Cont\,\Record{A;B}}}
+%     {\typ{\Gamma}{\Continue~W~V : B}}
+% \end{mathpar}
+% %
+% Both the domain and codomain of the continuation are the same as the
+% body type of function argument.
+Unlike $\Callcc$, captured continuations behave as functions.
 %
 \begin{reductions}
   \slab{Capture} &  \EC[\Callcomc~V] &\reducesto& \EC[V~\qq{\cont_{\EC}}]\\
-  % \slab{Resume}  &  \EC[\Continue~\cont_{\EC'}~V]  &\reducesto& \EC[\EC'[V]]
   \slab{Resume}  &  \Continue~\cont_{\EC}~V  &\reducesto& \EC[V]
 \end{reductions}
 %
+The capture rule for $\Callcomc$ is identical to the rule for
+$\Callcomc$, but the resume rule is different.
+%
 The effect of continuation invocation can be understood locally as it
 does not erase the global evaluation context, but rather composes with
 it.
@@ -1077,20 +1085,21 @@ In our framework both operators are value forms.
   V,W \in \ValCat ::= \cdots \mid \FelleisenC \mid \FelleisenF
 \]
 %
-The static semantics of $\FelleisenC$ are the same as $\Callcc$,
-whilst the static semantics of $\FelleisenF$ are the same as
-$\Callcomc$.
-\begin{mathpar}
-  \inferrule*
-    {~}
-    {\typ{\Gamma}{\FelleisenC : (\Cont\,\Record{A;\Zero} \to A) \to A}}
+% The static semantics of $\FelleisenC$ are the same as $\Callcc$,
+% whilst the static semantics of $\FelleisenF$ are the same as
+% $\Callcomc$.
+% \begin{mathpar}
+%   \inferrule*
+%     {~}
+%     {\typ{\Gamma}{\FelleisenC : (\Cont\,\Record{A;\Zero} \to A) \to A}}
 
-  \inferrule*
-    {~}
-    {\typ{\Gamma}{\FelleisenF : (\Cont\,\Record{A;A} \to A) \to A}}
-\end{mathpar}
+%   \inferrule*
+%     {~}
+%     {\typ{\Gamma}{\FelleisenF : (\Cont\,\Record{A;A} \to A) \to A}}
+% \end{mathpar}
 %
-The dynamic semantics of $\FelleisenC$ and $\FelleisenF$ also differ.
+The dynamic semantics of $\FelleisenC$ and $\FelleisenF$ are as
+follows.
 %
 \begin{reductions}
   \slab{C\textrm{-}Capture} &  \EC[\FelleisenC\,V] &\reducesto& V~\qq{\cont_{\EC}}\\
@@ -1187,28 +1196,28 @@ calling context.
 The particular application $\J\,(\lambda x.x)$ is so idiomatic that it
 has its own name: $\JI$, where $\keyw{I}$ is the identity function.
 
-Clearly, the return type of a continuation object produced by an $\J$
-application must be the same as the caller of $\J$. Thus to type $\J$
-we must track the type of calling context. Formally, we track the type
-of the context by extending the typing judgement relation with an
-additional singleton context $\Delta$. This context is modified by the
-typing rule for $\lambda$-abstraction and used by the typing rule for
-$\J$-applications. This is similar to type checking of return
-statements in statement-oriented programming languages.
-%
-\begin{mathpar}
-  \inferrule*
-    {\typ{\Gamma,x:A;B}{M : B}}
-    {\typ{\Gamma;\Delta}{\lambda x.M : A \to B}}
+% Clearly, the return type of a continuation object produced by an $\J$
+% application must be the same as the caller of $\J$. Thus to type $\J$
+% we must track the type of calling context. Formally, we track the type
+% of the context by extending the typing judgement relation with an
+% additional singleton context $\Delta$. This context is modified by the
+% typing rule for $\lambda$-abstraction and used by the typing rule for
+% $\J$-applications. This is similar to type checking of return
+% statements in statement-oriented programming languages.
+% %
+% \begin{mathpar}
+%   \inferrule*
+%     {\typ{\Gamma,x:A;B}{M : B}}
+%     {\typ{\Gamma;\Delta}{\lambda x.M : A \to B}}
 
-  \inferrule*
-    {~}
-    {\typ{\Gamma;B}{\J : (A \to B) \to \Cont\,\Record{A;B}}}
+%   \inferrule*
+%     {~}
+%     {\typ{\Gamma;B}{\J : (A \to B) \to \Cont\,\Record{A;B}}}
 
-  % \inferrule*
-  %   {\typ{\Gamma;\Delta}{V : A} \\ \typ{\Gamma;\Delta}{W : \Cont\,\Record{A;B}}}
-  %   {\typ{\Gamma;\Delta}{\Continue~W~V : B}}
-\end{mathpar}
+%   % \inferrule*
+%   %   {\typ{\Gamma;\Delta}{V : A} \\ \typ{\Gamma;\Delta}{W : \Cont\,\Record{A;B}}}
+%   %   {\typ{\Gamma;\Delta}{\Continue~W~V : B}}
+% \end{mathpar}
 %
 Any meaningful applications of $\J$ must appear under a
 $\lambda$-abstraction, because the application captures its caller's
@@ -1221,7 +1230,7 @@ annotate the evaluation contexts for ordinary applications.
   \slab{Resume}    & \EC[\Continue~\cont_{\Record{\EC';W}}\,V]  &\reducesto& \EC'[W\,V]
 \end{reductions}
 %
-\dhil{The continuation object should have time $\Cont\,\Record{A;\Zero}$}
+% \dhil{The continuation object should have time $\Cont\,\Record{A;\Zero}$}
 %
 The $\slab{Capture}$ rule only applies if the application of $\J$
 takes place inside an annotated evaluation context. The continuation
@@ -2132,16 +2141,31 @@ computation.
 
 If the reader ever find themselves in a quiz show asked to single out
 a canonical example of continuation use, then implementation of
-cooperative concurrency would be a qualified guess. Various forms of
-coroutines as continuations occur so frequently in the literature and
-in the wild that they have become routine.
+concurrency would be a qualified guess. Cooperative concurrency in
+terms of various forms of coroutines as continuations occur so
+frequently in the literature and in the wild that they have become
+routine.
 %
 \citet{HaynesFW86} published one of the first implementations of
-coroutines using first-class control. \citet{HiebD90} demonstrated how
-to implement engines. An engine is a kind of scheduler for
-computations running on a time budget~\cite{HaynesF84}.
+coroutines using first-class control.
 %
-Various other forms of schedulers were developed by \citet{GanzFW99}.
+Preemptive concurrency in the form of engines were implemented by
+\citet{DybvigH89}. An engine is a control abstraction that runs
+computations with an allotted time budget~\cite{HaynesF84}. They used
+continuations to represent strands of computation and timer interrupts
+to suspend continuations.
+%
+\citet{KiselyovS07a} used delimited continuations to explain various
+phenomena of operating systems, including multi-tasking.
+%
+On the web, \citet{Queinnec04} used continuations to model the
+client-server interactions. This model was adapted by
+\citet{CooperLWY06} in Links with support for an Erlang-style
+concurrency model~\cite{ArmstrongVW93}.
+%
+\citet{Leijen17a} and \citet{DolanEHMSW17} gave two different ways of
+implementing the asynchronous programming operator async/await as a
+user-definable library.
 
 Continuations have also been used in meta-programming to speed up
 partial evaluation and
@@ -2149,35 +2173,73 @@ multi-staging~\cite{LawallD94,KameyamaKS11,OishiK17,Yallop17}. Let
 insertion is a canonical example of use of continuations in
 multi-staging~\cite{Yallop17}.
 
-The aforementioned applications of continuations is by no means
-exhaustive, however, the diverse application spectrum underlines the
+Probabilistic programming is yet another application domain of
+continuations.  \citet{KiselyovS09} used delimited continuations to
+speed up probabilistic programs. \citet{GorinovaMH20} used
+continuations to achieve modularise probabilistic programs and to
+provide a simple and efficient mechanism for reparameterisation of
+inference algorithms.
+%
+In the subject of differentiable programming \citet{WangZDWER19}
+explained reverse-mode automatic differentiation operators in terms of
+delimited continuations.
+
+The aforementioned applications of continuations are by no means
+exhaustive, though, the diverse application spectrum underlines the
 versatility of continuations.
 
 \section{Constraining continuations}
 
-\citet{FriedmanH85} argued in favour of constraining the power of
-continuations~\cite{HaynesF87}. Although, they were concerned with
-callcc and undelimited continuations many of their arguments are
-applicable to other control operators and delimited continuations.
-
-For example callec is a variation of callcc where the continuation
-only can be invoked during the dynamic extent of
-callec~\cite{Flatt20}.
-
-Dynamic-wind\dots
-
-To avoid resource leakage the implementation of effect handlers in
-Multicore OCaml provides both a \emph{continue} primitive for
-continuing a given continuation and a \emph{discontinue} primitive for
-aborting a given continuation~\cite{DolanWSYM15,DolanEHMSW17}. The
-latter throws an exception at the operation invocation site to clean
-up resources.
+\citet{FriedmanH85} advocated for constraining the power of
+(undelimited) continuations~\cite{HaynesF87}.
 %
-A similar approached is used by \citet{Fowler19}, who uses a
+Even though, they were concerned with callcc and undelimited
+continuations some of their arguments are applicable to other control
+operators and delimited continuations.
+%
+For example, they argued in favour of restricting continuations to be
+one-shot, which means continuations may only be invoked once. Firstly,
+because one-shot continuations admit particularly efficient
+implementations. Secondly, many applications involve only single use
+of continuations. Thirdly, one-shot continuations interact more
+robustly with resources, such as file handles, than general multi-shot
+continuations, because multiple use of a continuation may accidentally
+interact with a resource after it has been released.
+
+One-shot continuations by themselves are no saving grace for avoiding
+resource leakage as they may be dropped or used to perform premature
+exits from a block with resources. For example, Racket provides the
+programmer with a facility known as \emph{dynamic-wind} to protect a
+context with resources such that non-local exits properly release
+whatever resources the context has acquired~\cite{Flatt20}.
+%
+An alternative approach is taken by Multicore OCaml, whose
+implementation of effect handlers with one-shot continuations provides
+both a \emph{continue} primitive for continuing a given continuation
+and a \emph{discontinue} primitive for aborting a given
+continuation~\cite{DolanWSYM15,DolanEHMSW17}. The latter throws an
+exception at the operation invocation site to which can be caught by
+local exception handlers to release resources properly.
+%
+This approach is also used by \citet{Fowler19}, who uses a
 substructural type system to statically enforce the use of
 continuations, either by means of a continue or a discontinue.
 
+% For example callec is a variation of callcc where continuation
+% invocation is only defined during the dynamic extent of
+% callec~\cite{Flatt20}.
+
 \section{Implementing continuations}
+
+There are numerous strategies for implementing continuations. There is
+no best implementation strategy. Each strategy has different
+trade-offs, and as such, there is no ``best'' strategy. In this
+section, I will briefly outline the gist of some implementation
+strategies and their trade-offs. For an in depth analysis the
+interested reader may consult the respective work of
+\citet{ClingerHO88} and \citet{FarvardinR20}, which contain thorough
+studies of implementation strategies for first-class continuations.
+%
 Table~\ref{tbl:ctrl-operators-impls} lists some programming languages
 with support for first-class control operators and their
 implementation strategies.
@@ -2208,7 +2270,7 @@ implementation strategies.
     \hline
     OchaCaml & shift/reset & Virtual machine\\
     \hline
-    Racket & callcc, callcc$^{\ast}$, cupto, fcontrol, control/prompt, shift/reset, splitter, spawn & Continuation marks\\
+    Racket & callcc, \textCallcomc{}, cupto, fcontrol, control/prompt, shift/reset, splitter, spawn & Segmented stacks\\
     \hline
     Rhino JavaScript      & JI                & Interpreter \\
     \hline
@@ -2216,21 +2278,85 @@ implementation strategies.
     \hline
     SML/NJ                & callcc            & CPS\\
     \hline
-    Wasm/k                & control/prompt    & ?? \\
+    Wasm/k                & control/prompt    & Virtual machine \\
     \hline
   \end{tabular}
-  \caption{Some languages and  their implementation strategies for first-class control.}\label{tbl:ctrl-operators-impls}
+  \caption{Some languages and their implementation strategies for continuations.}\label{tbl:ctrl-operators-impls}
+  \dhil{TODO: Figure out which implementation strategy Effekt uses}
 \end{table}
+%
+The control stack provides a adequate runtime representation of
+continuations as the contiguous sequence of activation records quite
+literally represent what to do next.
+%
+Thus continuation capture can be implemented by making a copy of the
+current stack (possibly up to some delimiter), and continuation
+invocation as reinstatement of the stack. This implementation strategy
+works well if continuations are captured infrequently. The MLton
+implementation of Standard ML utilises this strategy~\cite{Fluet20}.
+A slight variation is to defer the first copy action until the
+continuation is invoked, which requires marking the stack to remember
+which sequence of activation records to copy.
 
-\paragraph{Continuation marks}
+Obviously, frequent continuation use on top of a stack copying
+implementation can be expensive time wise as well as space wise,
+because with undelimited continuations multiple copies of the stack
+may be alive simultaneously.
+%
+Typically the prefix of copies will be identical, which suggests they
+ought to be shared. One way to achieve optimal sharing is to move from
+a contiguous stack to a non-contiguous stack representation,
+e.g. representing the stack as a heap allocated linked list of
+activation records~\cite{Danvy87}. With such a representation copying
+is a constant time and space operation, because there is no need to
+actually copy anything as the continuation is just a pointer into the
+stack.
+%
+The disadvantage of this strategy is that it turns every operation
+into an indirection.
 
-\paragraph{Continuation passing style}
+Segmented stacks provide a middle ground between contiguous stack and
+non-contiguous stack representations. With this representation the
+control stack is represented as a linked list of contiguous stacks
+which makes it possible to only copy a segment of the stack. The
+stacks grown and shrink dynamically as needed. This representation is
+due to \citet{HiebDB90}. It is used by Chez Scheme, which is the
+runtime that powers Racket~\cite{FlattD20}.
+%
+For undelimited continuations the basic idea is to create a pointer to
+the current stack upon continuation capture, and then allocate a new
+stack where subsequent computation happens.
+%
+For delimited continuations the control delimiter identify when a new
+stack should be allocated.
+%
+A potential problem with this representation is \emph{stack
+  thrashing}, which is a phenomenon that occurs when a stack is being
+continuously resized.
+%
+This problem was addressed by \citet{BruggemanWD96}, who designed a
+slight variation of segmented stacks optimised for one-shot
+continuations, which has been adapted by Multicore
+OCaml~\cite{DolanEHMSW17}.
 
-\paragraph{Abstract and virtual machines}
+\dhil{TODO: abstract machines}
 
-\paragraph{Segmented stacks}
+Continuation passing style (CPS) is a particular idiomatic notation
+for programs, where every aspect of control flow is made explicit,
+which makes it a good fit for implementing control abstractions.
+%
+Using trampolines CPS is even a viable strategy in environments that
+lack proper tail calls such as JavaScript~\cite{GanzFW99}.
 
-\paragraph{Stack copying}
+% \paragraph{Continuation marks}
+
+% \paragraph{Continuation passing style}
+
+% \paragraph{Abstract and virtual machines}
+
+% \paragraph{Segmented stacks}
+
+% \paragraph{Stack copying}
 
 \part{Design}