fcontrol WIP

macros.tex

@@ -452,3 +452,5 @@
 \newcommand{\cont}{\keyw{cont}}
 \newcommand{\Cont}{\dec{Cont}}
 \newcommand{\Algol}{Algol~60}
+\newcommand{\qq}[1]{\ensuremath{\ulcorner #1 \urcorner}}
+\newcommand{\prompttype}{\dec{Prompt}}

thesis.bib

@@ -1154,6 +1154,16 @@
 }
 
 # Structural Operational Semantics
+@techreport{Plotkin81,
+  author    = {Gordon D. Plotkin},
+  title     = {A structural approach to operational semantics},
+  number    = {FN-19},
+  school    = {Department of Computer Science, Aarhus University},
+  address   = {Aarhus, Denmark},
+  month     = sep,
+  year      = 1981
+}
+
 @article{Plotkin04a,
   author    = {Gordon D. Plotkin},
   title     = {A structural approach to operational semantics},
@@ -1161,9 +1171,9 @@
   volume    = {60-61},
   pages     = {17--139},
   year      = {2004},
-  timestamp = {Mon, 21 Feb 2005 12:50:35 +0100},
+  OPTtimestamp = {Mon, 21 Feb 2005 12:50:35 +0100},
-  biburl    = {https://dblp.org/rec/bib/journals/jlp/Plotkin04a},
+  OPTbiburl    = {https://dblp.org/rec/bib/journals/jlp/Plotkin04a},
-  bibsource = {dblp computer science bibliography, https://dblp.org}
+  OPTbibsource = {dblp computer science bibliography, https://dblp.org}
 }
 
 # Regular expressions
@@ -2013,3 +2023,188 @@
   pages     = {135--152},
   year      = {2000}
 }
+
+# CPS and abstract machine correspondences
+@inproceedings{DanvyN01,
+  author    = {Olivier Danvy and
+               Lasse R. Nielsen},
+  title     = {Defunctionalization at Work},
+  booktitle = {{PPDP}},
+  pages     = {162--174},
+  publisher = {{ACM}},
+  year      = {2001}
+}
+
+@inproceedings{AgerBDM03,
+  author    = {Mads Sig Ager and
+               Dariusz Biernacki and
+               Olivier Danvy and
+               Jan Midtgaard},
+  title     = {A functional correspondence between evaluators and abstract machines},
+  booktitle = {{PPDP}},
+  pages     = {8--19},
+  publisher = {{ACM}},
+  year      = {2003}
+}
+
+@inproceedings{Danvy04,
+  author    = {Olivier Danvy},
+  title     = {A Rational Deconstruction of Landin's {SECD} Machine},
+  booktitle = {{IFL}},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {3474},
+  pages     = {52--71},
+  publisher = {Springer},
+  year      = {2004}
+}
+
+@article{AgerDM04,
+  author    = {Mads Sig Ager and
+               Olivier Danvy and
+               Jan Midtgaard},
+  title     = {A functional correspondence between call-by-need evaluators and lazy
+               abstract machines},
+  journal   = {Inf. Process. Lett.},
+  volume    = {90},
+  number    = {5},
+  pages     = {223--232},
+  year      = {2004}
+}
+
+@inproceedings{Danvy04a,
+    author    = {Olivier Danvy},
+    title     = {On Evaluation Contexts, Continuations, and the Rest of Computation},
+    year      = {2004},
+    booktitle = {{CW}},
+    crossref  = {cw},
+}
+
+@techreport{cw,
+  author  =	 {Hayo Thielecke (Editor)},
+  title =	 {Proceedings of the Fourth {ACM} {SIGPLAN}
+                  Continuations Workshop {(CW'04)}},
+  number =	 {CSR-04-1},
+  institution =	 {School of Computer Science, University of
+                  Birmingham},
+  address =	 {Birmingham B15 2TT, United Kingdom},
+  year =	 2004,
+}
+
+@article{AgerDM05,
+  author    = {Mads Sig Ager and
+               Olivier Danvy and
+               Jan Midtgaard},
+  title     = {A functional correspondence between monadic evaluators and abstract
+               machines for languages with computational effects},
+  journal   = {Theor. Comput. Sci.},
+  volume    = {342},
+  number    = {1},
+  pages     = {149--172},
+  year      = {2005}
+}
+
+@article{DanvyM09,
+  author    = {Olivier Danvy and
+               Kevin Millikin},
+  title     = {Refunctionalization at work},
+  journal   = {Sci. Comput. Program.},
+  volume    = {74},
+  number    = {8},
+  pages     = {534--549},
+  year      = {2009}
+}
+
+# Answer type modification
+@article{Danvy98,
+  author    = {Olivier Danvy},
+  title     = {Functional Unparsing},
+  journal   = {J. Funct. Program.},
+  volume    = {8},
+  number    = {6},
+  pages     = {621--625},
+  year      = {1998}
+}
+
+@inproceedings{AsaiK07,
+  author    = {Kenichi Asai and
+               Yukiyoshi Kameyama},
+  title     = {Polymorphic Delimited Continuations},
+  booktitle = {{APLAS}},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {4807},
+  pages     = {239--254},
+  publisher = {Springer},
+  year      = {2007}
+}
+
+@inproceedings{KoboriKK16,
+  author    = {Ikuo Kobori and
+               Yukiyoshi Kameyama and
+               Oleg Kiselyov},
+  title     = {Answer-Type Modification without Tears: Prompt-Passing Style Translation
+               for Typed Delimited-Control Operators},
+  booktitle = {WoC},
+  series    = {{EPTCS}},
+  volume    = {212},
+  pages     = {36--52},
+  year      = {2015}
+}
+
+# Partial evaluation with control
+@inproceedings{LawallD94,
+  author    = {Julia L. Lawall and
+               Olivier Danvy},
+  title     = {Continuation-Based Partial Evaluation},
+  booktitle = {{LISP} and Functional Programming},
+  pages     = {227--238},
+  publisher = {{ACM}},
+  year      = {1994}
+}
+
+
+# Staging using control
+@article{KameyamaKS11,
+  author    = {Yukiyoshi Kameyama and
+               Oleg Kiselyov and
+               Chung{-}chieh Shan},
+  title     = {Shifting the stage - Staging with delimited control},
+  journal   = {J. Funct. Program.},
+  volume    = {21},
+  number    = {6},
+  pages     = {617--662},
+  year      = {2011}
+}
+
+@inproceedings{OishiK17,
+  author    = {Junpei Oishi and
+               Yukiyoshi Kameyama},
+  title     = {Staging with control: type-safe multi-stage programming with control
+               operators},
+  booktitle = {{GPCE}},
+  pages     = {29--40},
+  publisher = {{ACM}},
+  year      = {2017}
+}
+
+# Hindley-Milner type inference
+@article{Hindley69,
+ optISSN = {00029947},
+ optURL = {http://www.jstor.org/stable/1995158},
+ author = {Roger Hindley},
+ journal = {Transactions of the AMS},
+ pages = {29--60},
+ publisher = {{AMS}},
+ title = {The Principal Type-Scheme of an Object in Combinatory Logic},
+ volume = {146},
+ year = {1969}
+}
+
+@article{Milner78,
+  author    = {Robin Milner},
+  title     = {A Theory of Type Polymorphism in Programming},
+  journal   = {J. Comput. Syst. Sci.},
+  volume    = {17},
+  number    = {3},
+  pages     = {348--375},
+  year      = {1978}
+}

thesis.tex

@@ -844,7 +844,7 @@ An invocation of the continuation discards the invocation context and
 plugs the argument into the captured context.
 %
 \begin{reductions}
-  \slab{Capture} &  \EC[\Escape\;k\;\In\;M] &\reducesto& \EC[M[\cont_{\EC}/k]]\\
+  \slab{Capture} &  \EC[\Escape\;k\;\In\;M] &\reducesto& \EC[M[\qq{\cont_{\EC}}/k]]\\
   \slab{Resume}  &  \EC[\Continue~\cont_{\EC'}~V]  &\reducesto& \EC'[V]
 \end{reductions}
 %
@@ -883,7 +883,7 @@ the same.
 \end{mathpar}
 %
 \begin{reductions}
-  \slab{Capture} &  \EC[\Catch~k.M] &\reducesto& \EC[M[\cont_{\EC}/k]]\\
+  \slab{Capture} &  \EC[\Catch~k.M] &\reducesto& \EC[M[\qq{\cont_{\EC}}/k]]\\
   \slab{Resume}  &  \EC[\Continue~\cont_{\EC'}~V]  &\reducesto& \EC'[V]
 \end{reductions}
 %
@@ -930,7 +930,7 @@ 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~\cont_{\EC}]\\
+  \slab{Capture} &  \EC[\Callcc~V] &\reducesto& \EC[V~\qq{\cont_{\EC}}]\\
   \slab{Resume}  &  \EC[\Continue~\cont_{\EC'}~V]  &\reducesto& \EC'[V]
 \end{reductions}
 %
@@ -990,7 +990,7 @@ identical to the rule for $\Callcomc$, but the resume rule is
 different.
 %
 \begin{reductions}
-  \slab{Capture} &  \EC[\Callcomc~V] &\reducesto& \EC[V~\cont_{\EC}]\\
+  \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}
@@ -1090,9 +1090,9 @@ $\Callcomc$.
 The dynamic semantics of $\FelleisenC$ and $\FelleisenF$ also differ.
 %
 \begin{reductions}
-  \slab{C\textrm{-}Capture} &  \EC[\FelleisenC\,V] &\reducesto& V~\cont_{\EC}\\
+  \slab{C\textrm{-}Capture} &  \EC[\FelleisenC\,V] &\reducesto& V~\qq{\cont_{\EC}}\\
   \slab{C\textrm{-}Resume}  &  \EC[\Continue~\cont_{\EC'}~V]  &\reducesto& \EC'[V] \medskip\\
-  \slab{F\textrm{-}Capture} &  \EC[\FelleisenF\,V] &\reducesto& V~\cont_{\EC}\\
+  \slab{F\textrm{-}Capture} &  \EC[\FelleisenF\,V] &\reducesto& V~\qq{\cont_{\EC}}\\
   \slab{F\textrm{-}Resume}  &  \Continue~\cont_{\EC}~V  &\reducesto& \EC[V]
 \end{reductions}
 %
@@ -1214,7 +1214,7 @@ annotate the evaluation contexts for ordinary applications.
 %
 \begin{reductions}
   \slab{Annotate}   & \EC[(\lambda x.M)\,V] &\reducesto& \EC_\lambda[M[V/x]]\\
-  \slab{Capture}   & \EC_{\lambda}[\mathcal{D}[\J\,W]] &\reducesto& \EC_{\lambda}[\mathcal{D}[\cont_{\Record{\EC_{\lambda};W}}]]\\
+  \slab{Capture}   & \EC_{\lambda}[\mathcal{D}[\J\,W]] &\reducesto& \EC_{\lambda}[\mathcal{D}[\qq{\cont_{\Record{\EC_{\lambda};W}}}]]\\
   \slab{Resume}    & \EC[\Continue~\cont_{\Record{\EC';W}}\,V]  &\reducesto& \EC'[W\,V]
 \end{reductions}
 %
@@ -1325,6 +1325,11 @@ leads to the control phenomenon known as \emph{static delimited
   control}, where the control operator is statically bound by its
 delimiter.
 
+The machine interpretation and continuation passing style
+interpretation of composable continuations were eventually connected
+through defunctionalisation and refunctionalisation in a line of work
+by \citeauthor{Danvy04a} and
+collaborators~\cite{DanvyN01,AgerBDM03,Danvy04,AgerDM04,Danvy04a,AgerDM05,DanvyM09}.
 
 
 % The following year, \citet{DanvyF89} introduced an alternative pair of
@@ -1351,8 +1356,8 @@ delimiter.
 % %
 % \dhil{Consider dropping the blurb about hierarchy/meta layers.}
 
-Later a whole variety of alternative delimited control operators has
+Since control/prompt and shift/reset a whole variety of alternative
-appeared.
+delimited control operators has appeared.
 
 % Delimited control: Control delimiters form the basis for delimited
 % control. \citeauthor{Felleisen88} introduced control delimiters in
@@ -1442,7 +1447,7 @@ continuation invocation.
   \slab{Value} &
      \Prompt~V &\reducesto& V\\
   \slab{Capture} &
-     \Prompt~\EC[\Control~V] &\reducesto& \Prompt~(V~\cont_{\EC}), \text{ where $\EC$ contains no \Prompt}\\
+     \Prompt~\EC[\Control~V] &\reducesto& \Prompt~(V~\qq{\cont_{\EC}}), \text{ where $\EC$ contains no \Prompt}\\
   \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
 \end{reductions}
 %
@@ -1511,29 +1516,127 @@ discarded, because the continuation $k'$ is never invoked.
 %
 \dhil{Multi-prompts: more liberal typing, no interference}
 
-\paragraph{Cupto}
+\paragraph{\citeauthor{DanvyF90}'s shift and reset} Shift and reset
+first appeared in a technical report by \citeauthor{DanvyF89} in
+1989. Although, perhaps the most widely known account of shift and
+reset appeared in \citeauthor{DanvyF90}'s treatise on abstracting
+control the following year~\cite{DanvyF90}.
 %
-\begin{reductions}
+Shift and reset differ from control and prompt in that the contexts
-  \slab{Value} &
+abstracted by shift are statically scoped by reset.
-     \Set\; p \;\In\; V, \rho &\reducesto& V, \rho\\
-  \slab{New\textrm{-}prompt} &
-     \newPrompt, \rho &\reducesto& p, \rho \uplus \{p\}\\
-  \slab{Capture} &
-     \Set\; p \;\In\; \EC[\Cupto~p~k.M], \rho &\reducesto& M[\cont_{\EC}/k], \rho\\
-  \slab{Resume} & \Continue~\cont_{\EC}~V, \rho &\reducesto& \EC[V], \rho
-\end{reductions}
 
-\paragraph{\citeauthor{DanvyF90}'s shift and reset}
+% As with control and prompt, in our setting, shift appears as a value,
+% whilst reset appear as a computation.
+In our setting both shift and reset appear as computation forms.
+%
+\begin{syntax}
+ % & V, W &::=& \cdots \mid \shift\\
+ & M, N &::=& \cdots \mid \shift\; k.M \mid \reset{M}
+\end{syntax}
+%
+The $\shift$ construct captures the continuation delimited by an
+enclosing $\reset{-}$ and binds it to $k$ in the computation $M$.
+
+\citeauthor{DanvyF89}'s original development of shift and reset stands
+out from the previous developments of control operators, as they
+presented a type system for shift and reset, whereas previous control
+operators were originally studied in untyped settings.
+%
+The standard inference-based approach to type
+checking~\cite{Plotkin81,Plotkin04a} is inadequate for type checking
+shift and reset, because shift may alter the \emph{answer type} of the
+expression (the terminology `answer type' is adopted from typed
+continuation passing style transforms, where the codomain of every
+function is transformed to yield the type of whatever answer the
+entire program yields~\cite{MeyerW85}).
+%
+To capture the potent power of shift in the type system they
+introduced the notion of \emph{answer type
+  modification}~\cite{DanvyF89}.
+%
+The addition of answer type modification changes type judgement to be
+a five place relation.
+%
+\[
+  \typ{\Gamma;B}{M : A; B'}
+\]
+%
+This would be read as: in a context $\Gamma$ where the original result
+type was $B$, the type of $M$ is $A$, and modifies the result type to
+$B'$. In this system the typing rule for $\shift$ is as follows.
+%
+\begin{mathpar}
+  \inferrule*
+    {\typ{\Gamma,k : A / C \to B / C;D}{M : D;B'}}
+    {\typ{\Gamma;B}{\shift\;k.M : A;B'}}
+\end{mathpar}
+%
+Here the function type constructor $-/- \to -/-$ has been endowed with
+the domain and codomain of the continuation. The left hand side of
+$\to$ contains the domain type of the function and the codomain of the
+continuation, respectively. The right hand side contains the domain of
+the continuation and the codomain of the function, respectively.
+
+Answer type modification is a powerful feature that can be used to
+type embedded languages, an illustrious application of this is
+\citeauthor{Danvy98}'s typed $\dec{printf}$~\cite{Danvy98}. A
+polymorphic extension of answer type modification has been
+investigated by \citet{AsaiK07}, whilst \citet{KoboriKK16}
+demonstrated how to translate from a source language with answer type
+modification into a system without using typed multi-prompts.
+
+Differences between shift/reset and control/prompt manifests in the
+dynamic semantics as well.
 %
 \begin{reductions}
   \slab{Value}    & \reset{V}               &\reducesto& V\\
-  \slab{Capture}  & \reset{\EC[\shift\,k.M]} &\reducesto& \reset{M[\cont_{\EC}/k]}, \text { where $\EC$ contains no $\reset{-}$}\\
+  \slab{Capture}  & \reset{\EC[\shift\;k.M]} &\reducesto& \reset{M[\qq{\cont_{\EC}}/k]}, \text { where $\EC$ contains no $\reset{-}$}\\
   % \slab{Resume}   & \reset{\EC[\Continue~\cont_{\reset{\EC'}}~V]} &\reducesto& \reset{\EC[\reset{\EC'[V]}]}\\
   \slab{Resume}   & \Continue~\cont_{\EC}~V &\reducesto& \reset{\EC[V]}\\
 \end{reductions}
 %
-
+The $\slab{Value}$ and $\slab{Capture}$ rules are the same as for
+control/prompt (modulo the syntactic differences). The static nature
+of shift/reset manifests operationally in the $\slab{Resume}$ rule,
+where the reinstalled context $\EC$ gets enclosed in a new reset. The
+extra reset has ramifications for the operational behaviour of
+subsequent occurrences of $\shift$ in $\EC$. To put this into
+perspective, let us revisit the second control/prompt example with
+shift/reset instead.
 %
+\begin{derivation}
+  & 1 + \reset{2 + (\shift\;k.3 + k\,0) + (\shift\;k'.0)}\\
+  \reducesto^+& \reason{Capture $\EC = 2 + [\,] + (\shift\;k.0)$}\\
+  & 1 + \reset{\Continue~\cont_{\EC}~0}\\
+  \reducesto & \reason{Resume with 0}\\
+  & 1 + \reset{3 + \reset{2 + 0 + (\shift\;k'. 0)}}\\
+  \reducesto^+ & \reason{Capture $\EC' = 2 + [\,]$}\\
+  & 1 + \reset{3 + \reset{0}} \\
+  \reducesto^+ & \reason{\slab{Value} rule}\\
+  & 1 + \reset{3} \reducesto^+ 4 \\
+\end{derivation}
+%
+Contrast this result with the result $1$ obtained when using
+control/prompt. In essence the insertion of a new reset after
+resumption has the effect of remembering the local context of the
+first continuation invocation.
+
+This difference naturally raises the question whether shift/reset and
+control/prompt are interdefinable or exhibit essential expressivity
+differences. This question was answered by \citet{Shan04}, who
+demonstrated that shift/reset and control/prompt are
+macro-expressible. The translations are too intricate to be reproduced
+here, however, it is worth noting that \citeauthor{Shan04} were
+working in the untyped setting of Scheme and the translation of
+control/prompt made use of recursive
+continuations. \citet{BiernackiDS05} typed and reimplemented this
+translation in Standard ML New Jersey~\cite{AppelM91}, using
+\citeauthor{Filinski94}'s encoding of shift/reset in terms of callcc
+and state~\cite{Filinski94}.
+%
+%
+\dhil{Maybe mention the implication is that control/prompt has CPS semantics.}
+\dhil{Mention shift0/reset0, dollar0\dots}
 % \begin{reductions}
 %   % \slab{Value}    & \reset{V}               &\reducesto& V\\
 %   \slab{Capture}  & \reset{\EC[\shift\,k.M]} &\reducesto& M[\cont_{\reset{\EC}}/k]\\
@@ -1541,7 +1644,124 @@ discarded, because the continuation $k'$ is never invoked.
 % \end{reductions}
 %
 
-\paragraph{\citeauthor{PlotkinP09}'s effect handlers}
+\paragraph{\citeauthor{QueinnecS91}'s splitter}
+\begin{reductions}
+  \slab{Throw}   & \splitter~throw~calldc.\EC[\,throw~V] &\reducesto& V~\Unit\\
+  \slab{Capture} &
+     \splitter~throw~calldc.\EC[calldc~V] &\reducesto& V~\cont_{\EC} \\
+  \slab{Resume}  & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
+\end{reductions}
+
+
+\paragraph{Spawn}
+\dhil{TODO: Canonical reference \citet{HiebDA94}}
+
+\paragraph{\citeauthor{Sitaram93}'s fcontrol} The control operator
+`fcontrol' was introduced by \citet{Sitaram93} in 1993. The fcontrol
+operator distinguishes itself from the previous control operators in
+that it supports handling of continuations. \citeauthor{Sitaram93}'s
+observation was that previous control operators had hardwired handling
+of continuations into the capture mechanism, e.g. callcc applies its
+argument with the captured continuation. The programmer has no control
+over whether to function argument should be run immediately or run at
+all. \citeauthor{Sitaram93}'s goal was decouple the continuation
+capturing mechanism from the continuation handling mechanism.
+%
+\begin{syntax}
+  & V, W &::=& \cdots \mid \fcontrol\\
+  & M, N &::=& \cdots \mid \fprompt~V.M
+\end{syntax}
+%
+\begin{reductions}
+  \slab{Value} &
+     \fprompt~V.W &\reducesto& W\\
+  \slab{Capture} &
+     \fprompt~V.\EC[\fcontrol~W] &\reducesto& V~W~\cont_{\EC}, \text{ where $\EC$ contains no \fprompt}\\
+  \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
+\end{reductions}
+%
+
+\paragraph{Cupto} The control operator cupto is a variation of
+control0/prompt0 designed to fit into the typed ML-family of
+languages. It was introduced by \citet{GunterRR95} in 1995. The name
+cupto is an abbreviation for ``control up to''~\cite{GunterRR95}.
+%
+The control operator comes with a set of companion constructs, and
+thus, augments the syntactic categories of types, values, and
+computations.
+%
+\begin{syntax}
+  & A,B  &::=& \cdots \mid \prompttype~A \smallskip\\
+  & V,W  &::=& \cdots \mid p \mid \newPrompt\\
+  & M,N  &::=& \cdots \mid \Set\;V\;\In\;N \mid \Cupto~V~k.M
+\end{syntax}
+%
+The type $\prompttype~A$ is the type of prompts. It is parameterised
+by an answer type $A$ for the prompt context. Prompts are first-class
+values, which we denote by $p$. The construct $\newPrompt$ is a
+special function symbol, which returns a fresh prompt. The computation
+form $\Set\;V\;\In\;N$ activates the prompt $V$ to delimit the dynamic
+extent of continuations captured inside $N$. The $\Cupto~V~k.M$
+computation binds $k$ to the continuation up to (the first instance
+of) the active prompt $V$ in the computation $M$.
+
+\citet{GunterRR95} gave a Hindley-Milner type
+system~\cite{Hindley69,Milner78} for $\Cupto$, since they were working
+in the context of ML languages. I do not reproduce the full system
+here, only the essential rules for the $\Cupto$ constructs.
+%
+\begin{mathpar}
+  \inferrule*
+  {~}
+  {\typ{\Gamma,p:\prompttype~A}{p : \prompttype~A}}
+
+  \inferrule*
+  {~}
+  {\typ{\Gamma}{\newPrompt} : \UnitType \to \prompttype~A}
+
+  \inferrule*
+  {\typ{\Gamma}{V : \prompttype~A} \\ \typ{\Gamma}{N : A}}
+  {\typ{\Gamma}{\Set\;V\;\In\;N : A}}
+
+  \inferrule*
+  {\typ{\Gamma}{V : \prompttype~B} \\ \typ{\Gamma,k : A \to B}{M : B}}
+  {\typ{\Gamma}{\Cupto\;V\;k.M : A}}
+\end{mathpar}
+%
+%val cupto : 'b prompt -> (('a -> 'b) -> 'b) -> 'a
+%
+The typing rule for $\Set$ uses the type embedded in the prompt to fix
+the type of the whole computation $N$. Similarly, the typing rule for
+$\Cupto$ uses the prompt type of its value argument to fix the answer
+type for the continuation $k$.
+
+The dynamic semantics is generative to accommodate generation of fresh
+prompts. Formally, the reduction relation is augmented with a store
+$\rho$ that tracks which prompt names have already been allocated.
+%
+\begin{reductions}
+  \slab{Value} &
+     \Set\; p \;\In\; V, \rho &\reducesto& V, \rho\\
+  \slab{NewPrompt} &
+     \newPrompt~\Unit, \rho &\reducesto& p, \rho \uplus \{p\}\\
+  \slab{Capture} &
+  \Set\; p \;\In\; \EC[\Cupto~p~k.M], \rho &\reducesto& M[\qq{\cont_{\EC}}/k], \rho,\\
+  \multicolumn{4}{l}{\hfill\text{where $p$ is not active in $\EC$}}\\
+  \slab{Resume} & \Continue~\cont_{\EC}~V, \rho &\reducesto& \EC[V], \rho
+\end{reductions}
+%
+The $\slab{Value}$ rule is akin to value rules of shift/reset and
+control/prompt. The rule $\slab{NewPrompt}$ allocates a fresh prompt
+name $p$ and adds it to the store $\rho$. The $\slab{Capture}$ rule
+reifies and aborts the evaluation context up to the nearest enclosing
+active prompt $p$. After reification the prompt is removed and
+evaluation continues as $M$. The $\slab{Resume}$ rule reinstalls the
+captured context $\EC$ with the argument $V$ plugged in.
+%
+\dhil{Show some example of use\dots}
+
+\paragraph{\citeauthor{PlotkinP09}'s effect handlers} Effect handlers
+were introduced by \citet{PlotkinP09} in 2009.
 %
 \begin{reductions}
   \slab{Value}    & \Handle\; V \;\With\;H   &\reducesto& M[V/x], \text{ where } \{\Return\;x \mapsto M\} \in H\\
@@ -1593,17 +1813,6 @@ Shallow handlers can be used to simulate prompt and control.
 %
 %Recursive types are required to type the image of this translation
 
-\paragraph{\citeauthor{Sitaram93}'s fcontrol}
-%
-\begin{reductions}
-  \slab{Value} &
-     \fprompt~V.W &\reducesto& W\\
-  \slab{Capture} &
-     \fprompt~V.\EC[\fcontrol~W] &\reducesto& V~W~\cont_{\EC}, \text{ where $\EC$ contains no \fprompt}\\
-  \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
-\end{reductions}
-%
-
 \paragraph{\citeauthor{Longley09}'s catch-with-continue}
 %
 \begin{mathpar}
@@ -1620,18 +1829,6 @@ Shallow handlers can be used to simulate prompt and control.
   \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
 \end{reductions}
 
-\paragraph{\citeauthor{QueinnecS91}'s splitter}
-\begin{reductions}
-  \slab{Throw}   & \splitter~throw~calldc.\EC[\,throw~V] &\reducesto& V~\Unit\\
-  \slab{Capture} &
-     \splitter~throw~calldc.\EC[calldc~V] &\reducesto& V~\cont_{\EC} \\
-  \slab{Resume}  & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
-\end{reductions}
-
-
-\paragraph{Spawn}
-\dhil{TODO}
-
 \subsection{Second-class control operators}
 Coroutines, async/await, generators/iterators, amb.
 
@@ -1643,6 +1840,11 @@ Conway, who used coroutines as a code idiom in assembly
 programs~\cite{Knuth97}. Canonical reference for implementing
 coroutines with call/cc~\cite{HaynesFW86}.
 
+\section{Programming continuations}
+Blind vs non-blind backtracking. Engines. Web
+programming. Asynchronous
+programming. Coroutines. Meta-programming~\cite{LawallD94,KameyamaKS11,OishiK17,Yallop17}.
+
 \section{Constraining continuations}
 For example callec is a variation of callcc where the continuation
 only can be invoked during the dynamic extent of