WIP

thesis.bib

@@ -3739,3 +3739,14 @@
   pages     = {1--494},
   year      = 1894
 }
+
+# Game semantics
+@inbook{Hyland97,
+   author   = {Martin Hyland},
+   title    = {Game Semantics},
+   booktitle = {Semantics and Logics of Computation},
+   publisher = {Cambridge University Press},
+   editor   = {Andrew M. Pitts and Peter Dybjer},
+   pages    = {131--184},
+   year     = 1997
+}

thesis.tex

@@ -611,16 +611,33 @@ efficiency.
 % expressiveness.
 
 \section{Why first-class control matters}
+First things first, let us settle on the meaning of the qualifier
+`first-class'. A programming language entity (or citizen) is regarded
+as being first-class if it can be used on an equal footing with other
+entities.
+%
+A familiar example is functions as first-class values. A first-class
+function may be treated like any other primitive value, i.e. passed as
+an argument to other functions, returned from functions, stored in
+data structures, or let-bound.
+
+First-class control makes the control state of the program available
+as a first-class value known as a continuation object at any point
+during evaluation~\cite{FriedmanHK84}. This object comes equipped with
+at least one operation for restoring the control state. As such the
+control flow of the program becomes a first-class entity that the
+programmer may manipulate to implement interesting control phenomena.
+
 From the perspective of programmers first-class control is a valuable
 programming feature because it enables them to implement their own
-control idioms as if they were native to the programming language (in
-fact this is the very definition of first-class control). More
-important, with first-class control programmer-defined control idioms
-are local phenomena which can be encapsulated in a library such that
-the rest of the program does not need to be made aware of their
-existence. Conversely, without first-class control some control idioms
-can only be implemented using global program restructuring techniques
-such as continuation passing style.
+control idioms, such as async/await~\cite{SymePL11}, as if they were
+native to the programming language. More important, with first-class
+control programmer-defined control idioms are local phenomena which
+can be encapsulated in a library such that the rest of the program
+does not need to be made aware of their existence. Conversely, without
+first-class control some control idioms can only be implemented using
+global program restructuring techniques such as continuation passing
+style.
 
 From the perspective of compiler engineers first-class control is
 valuable because it unifies several control-related constructs under
@@ -678,9 +695,12 @@ intended purpose.
 
 In contrast, effect handlers provide a structured form of delimited
 control, where programmers can give distinct names to control reifying
-operations and separate the from their handling.
+operations and separate them from their handling. Throughout this
+dissertation we will see numerous examples of how effect handlers
+makes programming with delimited structured (c.f. the following
+section, Chapter~\ref{ch:continuations}, and
+Chapter~\ref{ch:unary-handlers}).
 %
-\dhil{Maybe expand this a bit more to really sell it}
 
 \section{State of effectful programming}
 \label{sec:state-of-effprog}
@@ -690,7 +710,8 @@ boxes, whose outputs are determined entirely by their
 inputs~\cite{Hughes89,Howard80}. This is a compelling view which
 admits a canonical mathematical model of
 computation~\cite{Church32,Church41}. Alas, this view does not capture
-the reality of practical programs, which interact their environment.
+the reality of practical programs, which interact with their
+environment.
 %
 Functional programming prominently features two distinct, but related,
 approaches to effectful programming, which \citet{Filinski96}
@@ -705,11 +726,11 @@ style~\cite{JonesW93}. The latter retains the usual direct style of
 programming either by hard-wiring the semantics of the effects into
 the language or by more flexible means via first-class control.
 
-In this section I will provide a brief programming perspective on
-different approaches to programming with effects along with an
-informal introduction to the related concepts. We will look at each
-approach through the lens of global mutable state --- which is the
-``hello world'' example of effectful programming.
+In this section I will provide a brief perspective on different
+approaches to programming with effects along with an informal
+introduction to the related concepts. We will look at each approach
+through the lens of global mutable state --- the ``hello world'' of
+effectful programming.
 
 % how
 % effectful programming has evolved as well as providing an informal
@@ -730,9 +751,9 @@ approach through the lens of global mutable state --- which is the
 %
 We can realise stateful behaviour by either using language-supported
 state primitives, globally structure our program to follow a certain
-style, or use first-class control in the form of delimited control to
-simulate state. We do not consider undelimited control, because it is
-insufficient to express mutable state~\cite{FriedmanS00}.
+style, or using first-class control in the form of delimited control
+to simulate state. We do not consider undelimited control, because it
+is insufficient to express mutable state~\cite{FriedmanS00}.
 % Programming in its infancy was effectful as the idea of first-class
 % control was conceived already during the design of the programming
 % language Algol~\cite{BackusBGKMPRSVWWW60} -- one of the early
@@ -777,13 +798,14 @@ It is common to find mutable state builtin into the semantics of
 mainstream programming languages. However, different languages vary in
 their approach to mutable state. For instance, state mutation
 underpins the foundations of imperative programming languages
-belonging to the C family of languages. They do typically not
+belonging to the C family of languages. They typically do not
 distinguish between mutable and immutable values at the level of
-types. Contrary, programming languages belonging to the ML family of
-languages use types to differentiate between mutable and immutable
-values. They reflect mutable values in types by using a special unary
-type constructor $\PCFRef^{\Type \to \Type}$. Furthermore, ML
-languages equip the $\PCFRef$ constructor with three operations.
+types. On the contrary, programming languages belonging to the ML
+family of languages use types to differentiate between mutable and
+immutable values. They reflect mutable values in types by using a
+special unary type constructor $\PCFRef^{\Type \to
+  \Type}$. Furthermore, ML languages equip the $\PCFRef$ constructor
+with three operations.
 %
 \[
   \refv : S \to \PCFRef~S \qquad\quad
@@ -815,7 +837,7 @@ The body of the function first retrieves the current value of the
 state cell and binds it to $st$. Subsequently, it destructively
 increments the value of the state cell. Finally, it applies the
 predicate $\even : \Int \to \Bool$ to the original state value to test
-whether its parity is even (remark: this example function is a slight
+whether its parity is even (this example function is a slight
 variation of an example by \citet{Gibbons12}).
 %
 We can run this computation as a subcomputation in the context of
@@ -913,8 +935,9 @@ represents the continuation of the invocation of $\shift$ (up to the
 innermost reset); it gets passed as a function to the argument of
 $\shift$.
 
-Both primitives are defined over some (globally) fixed result type
-$R$.
+We define both primitives over some fixed return type $R$ (an actual
+practical implementation would use polymorphism to make them more
+flexible).
 %
 By instantiating $R = S \to A \times S$, where $S$ is the type of
 state and $A$ is the type of return values, then we can use shift and
@@ -970,11 +993,12 @@ Modulo naming of operations, this version is similar to the version
 that uses builtin state. The type signature of the function is even
 the same.
 %
-Before we can apply this function we must first a state initialiser.
+Before we can apply this function we must first implement a state
+initialiser.
 %
 \[
   \bl
-    \runState : (\UnitType \to R) \to S \to R \times S\\
+    \runState : (\UnitType \to A) \to S \to A \times S\\
     \runState~m~st_0 \defas \reset{\lambda\Unit.\Let\;x \revto m\,\Unit\;\In\;\lambda st. \Record{x;st}}\,st_0
       \bl
       \el
@@ -994,7 +1018,7 @@ the state-accepting function returned by the reset instance. The
 application of the reset instance to $st_0$ effectively causes
 evaluation of each function in this chain to start.
 
-After instantiating $R = \Bool$ and $S = \Int$ we can use the
+After instantiating $A = \Bool$ and $S = \Int$ we can use the
 $\runState$ function to apply the $\incrEven$ function.
 %
 \[
@@ -1056,8 +1080,8 @@ Haskell~\cite{JonesABBBFHHHHJJLMPRRW99}.
     \el
   \]
   %
-  Interactions between $\Return$ and $\bind$ are governed by the
-  so-called `monad laws'.
+  Interactions between $\Return$ and $\bind$ are governed by the monad
+  laws.
   \begin{reductions}
     \slab{Left\textrm{ }identity} & \Return\;x \bind k &=& k~x\\
     \slab{Right\textrm{ }identity} & m \bind \Return &=& m\\
@@ -1397,7 +1421,7 @@ operation is another computation tree node.
   %
   \[
    \bl
-     \ba{@{~}l@{\qquad}@{~}r}
+     \ba{@{~}l@{\,\quad}@{~}r}
      \multicolumn{2}{l}{T~A \defas \Free~F~A} \smallskip\\
      \multirow{2}{*}{
        \bl
@@ -1894,10 +1918,13 @@ polymorphic $\lambda$-calculi for which I give computational
 interpretations in terms of contextual operational semantics and
 realise using two foundational operational techniques: continuation
 passing style and abstract machine semantics. When it comes to
-expressivity studies there are multiple complementary notions of
-expressiveness available in the literature; in this dissertation I
-work with typed macro-expressiveness and type-respecting
-expressiveness notions.
+expressiveness there are multiple possible dimensions to investigate
+and multiple different notions of expressivity available. I focus on
+two questions: `are deep, shallow, and parameterised handlers
+interdefinable?' which I investigate via a syntactic notion of
+expressiveness due \citet{Felleisen91}. And, `does effect handlers
+admit any essential computational efficiency?' which I investigate
+using a semantic notion of expressiveness due to \citet{LongleyN15}.
 
 \subsection{Scope extrusion}
 The literature on effect handlers is rich, and my dissertation is but
@@ -1941,8 +1968,11 @@ theory of scoped effect operations, whilst \citet{BiernackiPPS20}
 study them in conjunction with ordinary handlers from a programming
 perspective.
 
-% \citet{WuSH14} study scoped effects, which are effects whose payloads
-% are effectful computations
+% \citet{WuSH14} study scoped effects, which are effects whose
+% payloads are effectful computations. Scoped effects are
+% non-algebraic, Thinking in terms of computation trees, a scoped
+% effect is not an internal node of some computation tree, rather, it
+% is itself a whole computation tree.
 
 % Effect handlers were conceived in the realm of category theory to give
 % an algebraic treatment of exception handling~\cite{PlotkinP09}. They
@@ -1963,9 +1993,9 @@ handlers extension to Prolog; and \citet{Leijen17b} has an imperative
 take on effect handlers in C.
 
 \section{Contributions}
-The key contributions of this dissertation are scattered across the
-four main parts. The following listing summarises the contributions of
-each part.
+The key contributions of this dissertation are spread across the four
+main parts. The following listing summarises the contributions of each
+part.
 \paragraph{Background}
 \begin{itemize}
   \item A comprehensive operational characterisation of various
@@ -2010,35 +2040,40 @@ The following is a summary of the chapters belonging to each part of
 this dissertation.
 
 \paragraph{Background}
-Chapter~\ref{ch:maths-prep} defines some basic mathematical
+\begin{itemize}
+  \item Chapter~\ref{ch:maths-prep} defines some basic mathematical
 notation and constructions that are they pervasively throughout this
 dissertation.
 
-Chapter~\ref{ch:continuations} presents a literature survey of
+  \item Chapter~\ref{ch:continuations} presents a literature survey of
 continuations and first-class control. I classify continuations
 according to their operational behaviour and provide an overview of
 the various first-class sequential control operators that appear in
 the literature. The application spectrum of continuations is discussed
 as well as implementation strategies for first-class control.
+\end{itemize}
 
 \paragraph{Programming}
-Chapter~\ref{ch:base-language} introduces a polymorphic fine-grain
+\begin{itemize}
+  \item Chapter~\ref{ch:base-language} introduces a polymorphic fine-grain
 call-by-value core calculus, $\BCalc$, which makes key use of
 \citeauthor{Remy93}-style row polymorphism to implement polymorphic
 variants, structural records, and a structural effect system. The
 calculus distils the essence of the core of the Links programming
 language.
 
-Chapter~\ref{ch:unary-handlers} presents three extensions of $\BCalc$,
+  \item Chapter~\ref{ch:unary-handlers} presents three extensions of $\BCalc$,
 which are $\HCalc$ that adds deep handlers, $\SCalc$ that adds shallow
 handlers, and $\HPCalc$ that adds parameterised handlers. The chapter
 also contains a running case study that demonstrates effect handler
 oriented programming in practice by implementing a small operating
 system dubbed \OSname{} based on \citeauthor{RitchieT74}'s original
 \UNIX{}.
+\end{itemize}
 
 \paragraph{Implementation}
-Chapter~\ref{ch:cps} develops a higher-order continuation passing
+\begin{itemize}
+  \item Chapter~\ref{ch:cps} develops a higher-order continuation passing
 style translation for effect handlers through a series of step-wise
 refinements of an initial standard continuation passing style
 translation for $\BCalc$. Each refinement slightly modifies the notion
@@ -2047,18 +2082,20 @@ ultimately leads to the key invention of generalised continuation,
 which is used to give a continuation passing style semantics to deep,
 shallow, and parameterised handlers.
 
-Chapter~\ref{ch:abstract-machine} demonstrates an application of
+  \item Chapter~\ref{ch:abstract-machine} demonstrates an application of
 generalised continuations to abstract machine as we plug generalised
 continuations into \citeauthor{FelleisenF86}'s CEK machine to obtain
 an adequate abstract runtime with simultaneous support for deep,
 shallow, and parameterised handlers.
+\end{itemize}
 
 \paragraph{Expressiveness}
-Chapter~\ref{ch:deep-vs-shallow} shows that deep, shallow, and
+\begin{itemize}
+  \item Chapter~\ref{ch:deep-vs-shallow} shows that deep, shallow, and
 parameterised notions of handlers can simulate one another up to
 specific notions of administrative reduction.
 
-Chapter~\ref{ch:handlers-efficiency} studies the fundamental efficiency of effect
+  \item Chapter~\ref{ch:handlers-efficiency} studies the fundamental efficiency of effect
 handlers. In this chapter, we show that effect handlers enable an
 asymptotic improvement in runtime complexity for a certain class of
 functions. Specifically, we consider the \emph{generic count} problem
@@ -2068,9 +2105,12 @@ of $\BCalc$) and its extension with effect handlers $\HPCF$.
 We show that $\HPCF$ admits an asymptotically more efficient
 implementation of generic count than any $\BPCF$ implementation.
 %
+\end{itemize}
 
 \paragraph{Conclusions}
-Chapter~\ref{ch:conclusions} concludes and discusses future work.
+\begin{itemize}
+  \item Chapter~\ref{ch:conclusions} concludes and discusses future work.
+\end{itemize}
 
 
 \part{Background}
@@ -4189,6 +4229,8 @@ $\abort$ and $\calldc$ is only well-defined within the dynamic extent
 of $\splitter$. Since the prompt is eliminated after use of either
 operation subsequent operation invocations must be guarded by a new
 instance of $\splitter$.
+
+Let us consider an example using both $\calldc$ and $\abort$.
 %
 \begin{derivation}
   &2 + \splitter\,(\lambda p.2 + \splitter\,(\lambda p'.3 + \calldc\,\Record{p;\lambda k. k~0 + \abort\,\Record{p';\lambda\Unit.k~1}})),\emptyset\\
@@ -4210,11 +4252,12 @@ instance of $\splitter$.
 %
 The important thing to observe here is that the application of
 $\calldc$ skips over the inner prompt and reifies it as part of the
-continuation. The first application of $k$ restores the context with
-the prompt. The $\abort$ application erases the evaluation context up
-to this prompt, however, the body of the functional argument to
-$\abort$ reinvokes the continuation $k$ which restores the prompt
-context once again.
+continuation. This behaviour stands differ from the original
+formulations of control/prompt, shift/reset. The first application of
+$k$ restores the context with the prompt. The $\abort$ application
+erases the evaluation context up to this prompt, however, the body of
+the functional argument to $\abort$ reinvokes the continuation $k$
+which restores the prompt context once again.
 % \begin{derivation}
 %   &1 + \splitter\,(\lambda p.2 + \splitter\,(\lambda p'.3 + \calldc\,\Record{p';\lambda k. k\,0 + \calldc\,\Record{p';\lambda k'. k\,(k'\,1)}}))), \emptyset\\
 %   \reducesto& \reason{\slab{AppSplitter}}\\
@@ -4295,8 +4338,29 @@ rules. The interesting rule is the $\slab{Capture}$. When $\fcontrol$
 is applied to some value $W$ the enclosing context $\EC$ gets reified
 and aborted up to the nearest enclosing prompt, which invokes the
 handler $V$ with the argument $W$ and the continuation.
+
+Consider the following, slightly involved, example.
 %
-\dhil{Show an example\dots}
+\begin{derivation}
+  &2 + \fprompt\,(\lambda y~k'.1 + k'~y).\fprompt\,(\lambda x~k. x + k\,(\fcontrol~k)).3 + \fcontrol~1\\
+  \reducesto& \reason{\slab{Capture} $\EC = 3 + [\,]$}\\
+  &2 + \fprompt\,(\lambda y~k'.1 + k'~y).(\lambda x~k. x + k\,(\fcontrol~k))\,1\,\qq{\cont_{\EC}}\\
+  \reducesto^+& \reason{\slab{Capture} $\EC' = 1 + \qq{\cont_{\EC}}\,[\,]$}\\
+  &2 + (\lambda k~k'.k'\,(k~1))\,\qq{\cont_{\EC}}\,\qq{\cont_{\EC'}}\\
+  \reducesto^+& \reason{\slab{Resume} $\EC$ with $1$}\\
+  &2 + \qq{\cont{\EC'}}\,(3 + 1)\\
+  \reducesto^+& \reason{\slab{Resume} $\EC'$ with $4$}\\
+  &2 + 1 + \qq{\cont_{\EC}}\,4\\
+  \reducesto^+& \reason{\slab{Resume} $\EC$ with 4}\\
+  &3 + 3 + 4 \reducesto^+ 10
+\end{derivation}
+%
+This example makes use of nontrivial control manipulation as it passes
+a captured continuation around. However, the point is that the
+separation of the handling of continuations from their capture makes
+it considerably easier to implement complicated control idioms,
+because the handling code is compartmentalised.
+
 
 \paragraph{Cupto} The control operator cupto is a variation of
 control0/prompt0 designed to fit into the typed ML-family of
@@ -4350,18 +4414,18 @@ here, only the essential rules for the $\Cupto$ constructs.
 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 type of the $\Cupto$ expression is
-the same as the domain of the continuation, which at first glance may
-seem strange. The intuition is that $\Cupto$ behaves as a let binding
-for the continuation in the context of a $\Set$ expression, i.e.
-%
-\[
-  \bl
-    \Set\;p^{\prompttype~B}\;\In\;\EC[\Cupto\;p\;k^{A \to B}.M^B]^B\\
-    \reducesto \Let\;k \revto \lambda x^{A}.\EC[x]^B \;\In\;M^B
-  \el
-\]
-%
+type for the continuation $k$. % The type of the $\Cupto$ expression is
+% the same as the domain of the continuation, which at first glance may
+% seem strange. The intuition is that $\Cupto$ behaves as a let binding
+% for the continuation in the context of a $\Set$ expression, i.e.
+% %
+% \[
+%   \bl
+%     \Set\;p^{\prompttype~B}\;\In\;\EC[\Cupto\;p\;k^{A \to B}.M^B]^B\\
+%     \reducesto \Let\;k \revto \lambda x^{A}.\EC[x]^B \;\In\;M^B
+%   \el
+% \]
+% %
 
 The dynamic semantics is generative to accommodate generation of fresh
 prompts. Formally, the reduction relation is augmented with a store
@@ -4386,7 +4450,39 @@ 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}
+
+\citeauthor{GunterRR95}'s cupto provides similar behaviour to
+\citeauthor{QueinnecS91}'s splitter in regards to being able to `jump
+over prompt'. However, the separation of prompt creation from the
+control reifier coupled with the ability to set prompts manually
+provide a considerable amount of flexibility. For instance, consider
+the following example which illustrates how control reifier $\Cupto$
+may escape a matching control delimiter. Let us assume that two
+distinct prompts $p$ and $p'$ have already been created.
+%
+\begin{derivation}
+  &2 + \Set\; p \;\In\; 3 + \Set\;p'\;\In\;(\Set\;p\;\In\;\lambda\Unit.\Cupto~p~k.k\,(k~1))\,\Unit,\{p,p'\}\\
+  \reducesto& \reason{\slab{Value}}\\
+  &2 + \Set\; p \;\In\; 3 + \Set\;p'\;\In\;(\lambda\Unit.\Cupto~p~k.k\,(k~1))\,\Unit,\{p,p'\}\\
+  \reducesto^+& \reason{\slab{Capture} $\EC = 3 + \Set\;p'\;\In\;[\,]$}\\
+  &2 + \qq{\cont_{\EC}}\,(\qq{\cont_{\EC}}\,1),\{p,p'\}\\
+  \reducesto& \reason{\slab{Resume} $\EC$ with $1$}\\
+  &2 + \qq{\cont_{\EC}}\,(3 + \Set\;p'\;\In\;1),\{p,p'\}\\
+  \reducesto^+& \reason{\slab{Value}}\\
+  &2 + \qq{\cont_{\EC}}\,4,\{p,p'\}\\
+  \reducesto& \reason{\slab{Resume} $\EC$ with $4$}\\
+  &2 + \Set\;p'\;In\;4,\{p,p'\}\\
+  \reducesto& \reason{\slab{Value}}\\
+  &2 + 4,\{p,p'\} \reducesto 6,\{p,p'\}
+\end{derivation}
+%
+The prompt $p$ is used twice, and the dynamic scoping of $\Cupto$
+means when it is evaluated it reifies the continuation up to the
+nearest enclosing usage of the prompt $p$. Contrast this with the
+morally equivalent example using splitter, which would get stuck on
+the application of the control reifier, because it has escaped the
+dynamic extent of its matching delimiter.
+%
 
 \paragraph{\citeauthor{PlotkinP09}'s effect handlers} In 2009,
 \citet{PlotkinP09} introduced handlers for \citeauthor{PlotkinP01}'s
@@ -4663,49 +4759,75 @@ continuation without the handler.
 Chapter~\ref{ch:unary-handlers} contains further examples of deep and
 shallow handlers in action.
 %
-\dhil{Consider whether to present the below encodings\dots}
-%
-Deep handlers can be used to simulate shift0 and
-reset0~\cite{KammarLO13}.
-%
-\begin{equations}
-  \sembr{\shiftz~k.M} &\defas& \Do\;\dec{Shift0}~(\lambda k.M)\\
-  \sembr{\resetz{M}} &\defas&
-              \ba[t]{@{~}l}\Handle\;m\,\Unit\;\With\\
-                  ~\ba{@{~}l@{~}c@{~}l}
-                      \Return\;x &\mapsto& x\\
-                      \OpCase{\dec{Shift0}}{f}{k} &\mapsto& f\,k
-                   \ea
-              \ea
-\end{equations}
-%
+% \dhil{Consider whether to present the below encodings\dots}
+% %
+% Deep handlers can be used to simulate shift0 and
+% reset0~\cite{KammarLO13}.
+% %
+% \begin{equations}
+%   \sembr{\shiftz~k.M} &\defas& \Do\;\dec{Shift0}~(\lambda k.M)\\
+%   \sembr{\resetz{M}} &\defas&
+%               \ba[t]{@{~}l}\Handle\;m\,\Unit\;\With\\
+%                   ~\ba{@{~}l@{~}c@{~}l}
+%                       \Return\;x &\mapsto& x\\
+%                       \OpCase{\dec{Shift0}}{f}{k} &\mapsto& f\,k
+%                    \ea
+%               \ea
+% \end{equations}
+% %
 
-Shallow handlers can be used to simulate control0 and
-prompt0~\cite{KammarLO13}.
-%
-\begin{equations}
-  \sembr{\Controlz~k.M} &\defas& \Do\;\dec{Control0}~(\lambda k.M)\\
-  \sembr{\Promptz~M} &\defas&
-     \bl
-       prompt0\,(\lambda\Unit.M)\\
-       \textbf{where}\;
-         \bl
-            prompt0~m \defas
-              \ba[t]{@{~}l}\ShallowHandle\;m\,\Unit\;\With\\
-                  ~\ba{@{~}l@{~}c@{~}l}
-                      \Return\;x &\mapsto& x\\
-                      \OpCase{\dec{Control0}}{f}{k} &\mapsto& prompt0\,(\lambda\Unit.f\,k)
-                   \ea
-              \ea
-          \el
-      \el
-\end{equations}
+% Shallow handlers can be used to simulate control0 and
+% prompt0~\cite{KammarLO13}.
+% %
+% \begin{equations}
+%   \sembr{\Controlz~k.M} &\defas& \Do\;\dec{Control0}~(\lambda k.M)\\
+%   \sembr{\Promptz~M} &\defas&
+%      \bl
+%        prompt0\,(\lambda\Unit.M)\\
+%        \textbf{where}\;
+%          \bl
+%             prompt0~m \defas
+%               \ba[t]{@{~}l}\ShallowHandle\;m\,\Unit\;\With\\
+%                   ~\ba{@{~}l@{~}c@{~}l}
+%                       \Return\;x &\mapsto& x\\
+%                       \OpCase{\dec{Control0}}{f}{k} &\mapsto& prompt0\,(\lambda\Unit.f\,k)
+%                    \ea
+%               \ea
+%           \el
+%       \el
+% \end{equations}
 %
 %Recursive types are required to type the image of this translation
 
 \paragraph{\citeauthor{Longley09}'s catch-with-continue}
 %
-\dhil{TODO}
+The control operator \emph{catch-with-continue} (abbreviated
+catchcont) is a delimited extension of the $\Catch$ operator. It was
+designed by \citet{Longley09} in 2008~\cite{LongleyW08}. Its origin is
+in game semantics, in which program evaluation is viewed as an
+interactive dialogue with the ambient environment~\cite{Hyland97} ---
+this view aligns neatly with the view of effect handler oriented
+programming. Curiously, \citeauthor{Longley09} and
+\citeauthor{PlotkinP09} developed catchcont and effect handlers,
+respectively, during the same time, in the same country, in the same
+city, in the same building. Despite all of this the two operators have
+not yet been related formally.
+
+The catchcont operator appears as a computation form in our calculus.
+%
+\begin{syntax}
+   &M,N \in \CompCat &::=& \cdots \mid \Catchcont~f.M
+\end{syntax}
+%
+Unlike other delimited control operators, $\Catchcont$ does not
+introduce separate explicit syntactic constructs for the control
+delimiter and control reifier. Instead it leverages the higher-order
+facilities of $\lambda$-calculus: the syntactic construct $\Catchcont$
+play the role of control delimiter and the name $f$ of function type
+is the name of the control reifier. \citet{LongleyW08} describe $f$ as
+a `dummy variable'.
+
+The typing rule for $\Catchcont$ is as follows.
 %
 \begin{mathpar}
   \inferrule*
@@ -4713,6 +4835,20 @@ prompt0~\cite{KammarLO13}.
     {\typ{\Gamma}{\Catchcont\;f.M : C \times ((A \to B) \to D) + (A \times (B \to (A \to B) \to C \times D))}}
 \end{mathpar}
 %
+The computation handled by $\Catchcont$ must return a pair, where the
+first component must be a ground value. This restriction ensures that
+the value is not a $\lambda$-abstraction, which means that the value
+cannot contain any further occurrence of the control reifier $f$. The
+second component is unrestricted, and thus, it may contain further
+occurrences of $f$.  If $M$ fully reduces then $\Catchcont$ returns a
+pair consisting of a ground value (i.e. an answer from $M$) and a
+continuation function which allow $M$ to yield further
+`answers'. Alternatively, if $M$ invokes the control reifier $f$, then
+$\Catchcont$ returns a pair consisting of the argument supplied to $f$
+and the current continuation of the invocation of $f$.
+
+The operational rules for $\Catchcont$ are as follows.
+%
 \begin{reductions}
   \slab{Value} &
      \Catchcont \; f . \Record{V;W} &\reducesto& \Inl\; \Record{V;\lambda\,f. W}\\
@@ -4720,7 +4856,15 @@ prompt0~\cite{KammarLO13}.
      \Catchcont \; f .\EC[\,f\,V]   &\reducesto& \Inr\; \Record{V; \lambda x. \lambda f. \Continue~\cont_{\EC}~x}\\
   \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
 \end{reductions}
-
+%
+The \slab{Value} makes sure to bind any lingering instances of $f$ in
+$W$ before escaping the delimiter. The \slab{Capture} rule reifies and
+aborts the current evaluation up to, but no including, the delimiter,
+which gets uninstalled. The reified evaluation context gets stored in
+the second component of the returned pair. Importantly, the second
+$\lambda$-abstraction makes sure to bind any instances of $f$ in the
+captured evaluation context once it has been reinstated by the
+\slab{Resume} rule.
 % \subsection{Second-class control operators}
 % Coroutines, async/await, generators/iterators, amb.
 
@@ -15010,8 +15154,9 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
   % By case analysis on $\reducesto$ and induction on $\approxa$ using
   % Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
   %
-  By induction on $M' \approxa \sdtrans{M}$ and side induction on
-  $M \reducesto N$ using Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
+  By induction on $M' \approxa \sdtrans{M}$ and case analysis on
+  $M \reducesto N$ using Lemma~\ref{lem:sdtrans-subst} and
+  Lemma~\ref{lem:sdtrans-admin}.
   %
   The interesting case is reflexivity of $\approxa$ where
   $M \reducesto N$ is an application of $\semlab{Op^\dagger}$, which