Example

macros.tex

@@ -23,6 +23,8 @@
 \newcommand{\SC}{\ensuremath{\mathsf{S}}}
 \newcommand{\ST}{\ensuremath{\mathsf{T}}}
 \newcommand{\ar}{\ensuremath{\mathsf{ar}}}
+\newcommand{\Tm}{\ensuremath{\mathsf{Tm}}}
+\newcommand{\Ty}{\ensuremath{\mathsf{Ty}}}
 
 %%
 %% Partiality
@@ -528,11 +530,11 @@
 \newcommand{\Catchcont}{\keyw{catchcont}}
 \newcommand{\Control}{\keyw{control}}
 \newcommand{\Prompt}{\#}
-\newcommand{\Controlz}{\keyw{control0}}
-\newcommand{\Promptz}{\#_0}
+\newcommand{\Controlz}{\ensuremath{\keyw{control_0}}}
+\newcommand{\Promptz}{\ensuremath{\#_0}}
 \newcommand{\Escape}{\keyw{escape}}
 \newcommand{\shift}{\keyw{shift}}
-\newcommand{\shiftz}{\keyw{shift0}}
+\newcommand{\shiftz}{\ensuremath{\keyw{shift_0}}}
 \def\sigh#1{%
 \pmb{\left\langle\vphantom{#1}\right.}%
 #1%
@@ -540,6 +542,8 @@
 \newcommand{\llambda}{\ensuremath{\pmb{\lambda}}}
 \newcommand{\reset}[1]{\pmb{\langle} #1 \pmb{\rangle}}
 \newcommand{\resetz}[1]{\pmb{\langle} #1 \pmb{\rangle}_0}
+\newcommand{\dollarz}[2]{\ensuremath{\reset{#2 \mid #1}}}
+\newcommand{\dollarzh}[2]{\ensuremath{#1\,\$_0#2}}
 \newcommand{\fcontrol}{\keyw{fcontrol}}
 \newcommand{\fprompt}{\%}
 \newcommand{\splitter}{\keyw{splitter}}

thesis.bib

@@ -1802,6 +1802,18 @@
   year      = {1990}
 }
 
+@inproceedings{KameyamaY08,
+  author    = {Yukiyoshi Kameyama and
+               Takuo Yonezawa},
+  title     = {Typed Dynamic Control Operators for Delimited Continuations},
+  booktitle = {{FLOPS}},
+  series    = {{LNCS}},
+  volume    = {4989},
+  pages     = {239--254},
+  publisher = {Springer},
+  year      = {2008}
+}
+
 # Escape
 @article{Reynolds98a,
   author    = {John C. Reynolds},

thesis.tex

@@ -232,10 +232,10 @@
   expressiveness that affirms the existence of encodings between
   handlers, but it provides no information about the computational
   content of the encodings. Second, using the semantic notion of
-  \emph{type-respecting expressiveness} I show that for a class of
-  programs a programming language with first-class control
-  (e.g. effect handlers) admits asymptotically faster implementations
-  than possible in a language without first-class control.
+  expressiveness I show that for a class of programs a programming
+  language with first-class control (e.g. effect handlers) admits
+  asymptotically faster implementations than possible in a language
+  without first-class control.
 %
 }
 
@@ -1937,8 +1937,12 @@ deep handlers, which provide a form of lexical scoping for effect
 operations, thus statically binding them to their handlers.
 %
 \citeauthor{Geron19}'s PhD dissertation develops the mathematical
-theory of scoped effect operations, whilst \citet{WuSH14} and
-\citet{BiernackiPPS20} study them from a programming perspective.
+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
 
 % Effect handlers were conceived in the realm of category theory to give
 % an algebraic treatment of exception handling~\cite{PlotkinP09}. They
@@ -1950,13 +1954,13 @@ either added language-level support for handlers~
 or embedded them in
 libraries~\cite{KiselyovSS13,KiselyovI15,KiselyovS16,KammarLO13,BrachthauserS17,Brady13,XieL20}. Thus
 functional perspectives on effect handlers are plentiful in the
-literature. There are only a a few takes on effect handlers outside
-functional programming: \citeauthor{Brachthauser20}'s PhD dissertation
-contains an object-oriented perspective on effect handlers in
-Java~\cite{Brachthauser20}; \citeauthor{Saleh19}'s PhD dissertation
-offers a logic programming perspective via an effect handlers
-extension to Prolog; and \citet{Leijen17b} has an imperative take on
-effect handlers in C.
+literature. Some notable examples of perspectives on effect handlers
+outside functional programming are: \citeauthor{Brachthauser20}'s PhD
+dissertation, which contains an object-oriented perspective on effect
+handlers in Java~\cite{Brachthauser20}; \citeauthor{Saleh19}'s PhD
+dissertation offers a logic programming perspective via an effect
+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
@@ -2092,15 +2096,15 @@ recommend \citeauthor{Harper16}'s book \emph{Practical Foundations for
   Programming Languages}~\cite{Harper16} (do not let the ``practical''
 qualifier deceive you) --- the two books complement each other nicely.
 
-\section{Relations and functions}
-\label{sec:functions}
+\section{Relations}
+\label{sec:relations}
 
-Relations and functions feature prominently in the design and
-understanding of the static and dynamic properties of programming
-languages. The interested reader is likely to already be familiar with
-the basic concepts of relations and functions, although this section
-briefly introduces the concepts, its purpose is to introduce the
-notation that I am using pervasively throughout this dissertation.
+Relations feature prominently in the design and understanding of the
+static and dynamic properties of programming languages. The interested
+reader is likely to already be familiar with the basic concepts of
+relations, although this section briefly introduces the concepts, its
+real purpose is to introduce the notation that I am using pervasively
+throughout this dissertation.
 %
 
 I assume familiarity with basic set theory.
@@ -2123,7 +2127,7 @@ this raises the question in which order the product operator
 taken to be right associative, meaning
 $A \times B \times C = A \times (B \times C)$.
 %
-\dhil{Define tuples (and ordered pairs)?}
+%\dhil{Define tuples (and ordered pairs)?}
 %
 % To make the notation more compact for the special case of $n$-fold
 % product of some set $A$ with itself we write
@@ -2138,7 +2142,7 @@ $A \times B \times C = A \times (B \times C)$.
   An element $a \in A$ is related to an element $b \in B$ if
   $(a, b) \in R$, sometimes written using infix notation $a\,R\,b$.
   %
-  If $A = B$ then $R$ is said to be a homogeneous relation.
+  If $A = B$ then $R$ is said to be a \emph{homogeneous} relation.
 \end{definition}
 %
 
@@ -2218,7 +2222,10 @@ related to one $b \in B$. Note this does not mean that every $a$
 \emph{is} related to some $b$. The serial property guarantees that
 every $a \in A$ is related to one or more elements in $B$.
 %
-We use these properties to define partial and total functions.
+
+\section{Functions}
+\label{sec:functions}
+We define partial and total functions in terms of relations.
 %
 \begin{definition}
   A partial function $f : A \pto B$ is a functional relation
@@ -2259,7 +2266,6 @@ written $\dec{Im}(f)$, is the set of values that it can return, i.e.
     \dec{Im}(f) \defas \{\, f(a) \mid a \in \dom(f) \}.
 \]
 
-
 \begin{definition}
   A function $f : A \to B$ is injective and surjective if it satisfies
   the following criteria, respectively.
@@ -2330,211 +2336,242 @@ of growth of $f$ is constant.
   \]
 \end{definition}
 
-\section{Typed programming languages}
-\label{sec:pls}
-We will be working mostly with statically typed programming
-languages. The following definition informally describes the core
-components used to construct a statically typed programming language.
-%
-The objective here is not to be mathematical
-rigorous.% but rather to give
-% an idea of what constitutes a programming language.
-%
-\begin{definition}
-  A statically typed programming language $\LLL$ consists of a syntax
-  $S$, static semantics $T$, and dynamic semantics $E$ where
-  \begin{itemize}
-  \item $S$ is a collection of syntax constructors $\SC_1,\SC_2,\dots$
-    constructing members of each syntactic category of $\LLL$
-    (e.g. terms, types, and kinds);
-  \item $T : S \to \B$ is \emph{typechecking} function, which decides
-    whether a given (closed) term is well-typed; and
-  \item $E : P \pto R$ is an \emph{evaluation} function, which maps
-    well-typed programs $P \subseteq S$ to some unspecified set of
-    answers $R$.
-  \end{itemize}
-\end{definition}
-%
-We will always present the syntax of a programming language on
-Backus-Naur form.
-%
-The static semantics will always be given in form a typing judgement
-(and a kinding judgement for languages with polymorphism), and the
-dynamic semantics will be given as either a reduction relation or an
-abstract machine.
+% \section{Typed programming languages}
+% \label{sec:pls}
+% We will be working mostly with statically typed programming
+% languages. The following definition informally describes the core
+% components used to construct a statically typed programming language.
+% %
+% The objective here is not to be mathematical
+% rigorous.% but rather to give
+% % an idea of what constitutes a programming language.
+% %
+% \begin{definition}
+%   A statically typed programming language $\LLL$ consists of a syntax
+%   $S$, static semantics $T$, and dynamic semantics $E$ where
+%   \begin{itemize}
+%   \item $S$ is a collection of, possibly mutually, inductively defined
+%     syntactic categories (e.g. terms, types, and kinds). Each
+%     syntactic category contains a collection of syntax constructors
+%     with nonnegative arities $\{(\SC_i,\ar_i)\}$ which construct
+%     abstract syntax trees. We insist that $S$ contains at least two
+%     syntactic categories for constructing terms and types of
+%     $\LLL$. We write $\Tm(S)$ for the terms category and $\Ty(S)$ for
+%     the types category;
+%   \item $T : \Tm(S) \times \Ty(S) \to \B$ is \emph{typechecking}
+%     function, which decides whether a given term is well-typed; and
+%   \item $E : P \pto R$ is an \emph{evaluation} function, which maps
+%     well-typed programs
+%     \[
+%       P \defas \{ M \in \Tm(S) \mid A \in \Ty(S), T(M, A)~\text{is true} \},
+%     \]
+%     to some unspecified set of answers $R$.
+%   \end{itemize}
+% \end{definition}
+% %
+% We will always present the syntax of a programming language on
+% Backus-Naur form.
+% %
+% The static semantics will always be given in form a typing judgement
+% (and a kinding judgement for languages with polymorphism), and the
+% dynamic semantics will be given as either a reduction relation or an
+% abstract machine.
 
-We will take the view that an untyped programming language is a
-special instance of a statically typed programming language, where the
-typechecking function $T$ is the constant function that always returns
-true.
+% We will take the view that an untyped programming language is a
+% special instance of a statically typed programming language, where the
+% typechecking function $T$ is the constant function that always returns
+% true.
 
-Often we will build programming languages incrementally by starting
-from a base language and extend it with new facilities. A
-\emph{conservative extension} is a particularly well-behaved extension
-in the sense that it preserves the all of the behaviour of the
-original language.
-%
-\begin{definition}
-  A programming language $\LLL = (S, T, E)$ is said to be a
-  \emph{conservative extension} of a language $\LLL' = (S', T', E')$
-  if the following conditions are met.
-  \begin{itemize}
-    \item $S'$ is a proper subset of $S$.
-    \item $\LLL$ preserves the static semantics of $\LLL'$,
-      i.e. $T(p)$ holds if and only if $T'(p)$ holds for all programs
-      $p$ generated by $S'$.
-    \item $\LLL$ preserves the dynamic semantics of $\LLL'$, i.e.
-      $E(p)$ holds if and only if $E'(p)$ holds for all programs $p$
-      generated by $S'$.
-  \end{itemize}
-  Conversely, $\LLL'$ is a \emph{conservative restriction} of $\LLL$.
-\end{definition}
+% Often we will build programming languages incrementally by starting
+% from a base language and extend it with new facilities. A
+% \emph{conservative extension} is a particularly well-behaved extension
+% in the sense that it preserves the all of the behaviour of the
+% original language.
+% %
+% \begin{definition}
+%   A programming language $\LLL = (S, T, E)$ is said to be a
+%   \emph{conservative extension} of a language $\LLL' = (S', T', E')$
+%   if the following conditions are met.
+%   \begin{itemize}
+%     \item $\LLL$ syntactically extends $\LLL'$, i.e. $S'$ is a proper
+%       subset of $S$.
+%     \item $\LLL$ preserves the static semantics and dynamic semantics
+%       of $\LLL'$, that is $T(M, A) = T'(M, A)$ and $E(M)$ holds if and
+%       only if $E'(M)$ holds for all types $A \in \Ty(S)$ and programs
+%       $M \in \Tm(S)$.
+%   \end{itemize}
+%   Conversely, $\LLL'$ is a \emph{conservative restriction} of $\LLL$.
+% \end{definition}
 
-We will be using a typed variation of \citeauthor{Felleisen91}'s
-macro-expressivity to compare the relative expressiveness of different
-kinds of effect
-handlers~\cite{Felleisen90,Felleisen91}. Macro-expressivity is a
-syntactic notion based on the idea of macro rewrites as found in the
-programming language Scheme~\cite{SperberDFSFM10}.
-%
-\begin{definition}[Typability-preserving macro-expressiveness]
-  Let both $\LLL = (S, T, E)$ and $\LLL' = (S', T', E')$ be
-  programming languages such that $\SC_1,\dots,\SC_k \in S$ but
-  $\SC_1,\dots,\SC_k \notin S'$. If there exists a translation on
-  syntax constructors $\sembr{-} : S \to S'$ that is homomorphic on
-  all syntax constructors but $\SC_1,\dots,\SC_k$, such that for all
-  $p$ programs generated by $S$
-  %
-  \[
-    \ba{@{~}l@{~}l}
-             &T(p)~\text{holds if and only if}~T'(\sembr{p})~\text{holds}, \\
-             \text{and}& E(p)~\text{holds if and only if}~E'(\sembr{p})~\text{holds}
-    \ea
-  \]
-  %
-  then we say that $\LLL'$ can \emph{macro-express} the
-  $\SC_1,\dots,\SC_k$ facilities of $\LLL$.
-\end{definition}
-%
-% In essence, if $\LLL$ admits a translation into a sublanguage $\LLL'$
+% We will often work with translations on syntax between languages. It
+% is often the case that a syntactic translation is \emph{homomorphic}
+% on most syntax constructors, which is a technical way of saying it
+% does not perform any interesting transformation on those
+% constructors. Therefore we will omit homomorphic cases in definitions
+% of translations.
+% %
+% \begin{definition}
+%   Let $\LLL = (S, T, E)$ and $\LLL' = (S', T', E')$ be programming
+%   languages. A translation $\sembr{-} : S \to S'$ on the syntax
+%   between $\LLL$ and $\LLL'$ is a homomorphism if it distributes over
+%   the syntax constructors, i.e. for every $\{(\SC_i,\ar_i)\}_i \in S$
+%   \[
+%     \sembr{\SC_i(t_1,\dots,t_{\ar_i})} = \sembr{\SC_i}(\sembr{t_1},\cdots,\sembr{t_{\ar_i}}),
+%   \]
+%   %
+%   where $t_1,\dots,t_{\ar_i}$ are abstract syntax trees. We say that
+%   $\sembr{-}$ is homomorphic on $S_i$.
+% \end{definition}
+
+% We will be using a typed variation of \citeauthor{Felleisen91}'s
+% macro-expressivity to compare the relative expressiveness of different
+% languages~\cite{Felleisen90,Felleisen91}. Macro-expressivity is a
+% syntactic notion based on the idea of macro rewrites as found in the
+% programming language Scheme~\cite{SperberDFSFM10}.
+% %
+% Informally, if $\LLL$ admits a translation into a sublanguage $\LLL'$
 % in a way which respects not only the behaviour of programs but also
-% aspects of their local syntactic structure, then $\LLL'$
-% macro-expresses $\LLL$. If the translation of some $\LLL$-program into
-% $\LLL'$ requires a complete global restructuring, we may say that
-% $\LLL'$ is in some way less expressive than $\LLL$.
-In general, it is not the case that $\sembr{-}$ preserves types, it is
-only required to ensure that the translated term $p$ is typable in
-the target language $\LLL'$
-
-% \dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness~\cite{Felleisen90,Felleisen91}}
-
-% \begin{definition}
-%   A signature $\Sigma$ is a collection of abstract syntax constructors
-%   with arities $\{(\SC_i, \ar_i)\}_i$, where $\ST_i$ are syntactic
-%   entities and $\ar_i$ are natural numbers. Syntax constructors with
-%   arities $0$, $1$, $2$, and $3$ are referred to as nullary, unary,
-%   binary, and ternary, respectively.
-% \end{definition}
-
-% \begin{definition}[Terms in contexts]
-%   A context $\mathcal{X}$ is set of variables $\{x_1,\dots,x_n\}$. For
-%   a signature $\Sigma = \{(\SC_i, \ar_i)\}_i$ the $\Sigma$-terms in
-%   some context $\mathcal{X}$ are generated according to the following
-%   inductive rules:
-%   \begin{itemize}
-%     \item each variable $x_i \in \mathcal{X}$ is a $\Sigma$-term,
-%     \item if $t_1,\dots,t_{\ar_i}$ are $\Sigma$-terms in context
-%       $\mathcal{X}$, then $\SC_i(t_1,\dots,t_{\ar_i})$ is
-%       $\Sigma$-term in context $\mathcal{X}$.
-%     \end{itemize}
-%     We write $\mathcal{X} \vdash t$ to indicate that $t$ is a
-%     $\Sigma$-term in context $\mathcal{X}$. A $\Sigma$-term $t$ is
-%     said to be closed if $\emptyset \vdash t$, i.e. no variables occur
-%     in $t$.
-% \end{definition}
-
-% \begin{definition}
-%   A $\Sigma$-equation is a pair of terms $t_1,t_2 \in \Sigma$ in
-%   context $\mathcal{X}$, which we write as
-%   $\mathcal{X} \vdash t_1 = t_2$.
-% \end{definition}
-
-% The notation $\mathcal{X} \vdash t_1 = t_2$ begs to be read as a
-% logical statement, though, in universal algebra the notation is simply
-% a syntax. In order to give it a meaning we must first construct a
-% \emph{model} which interprets the syntax. We shall not delve deeper
-% here; for our purposes we may think of a $\Sigma$-equation as a
-% logical statement (the attentive reader may already have realised that .
-
-
-% The following definition is an adaptation of
-% \citeauthor{Felleisen90}'s definition of programming language to
-% define statically typed programming languages~\cite{Felleisen90}.
+% their local syntactic structure, then $\LLL'$ macro-expresses
+% $\LLL$. % If the translation of some $\LLL$-program into $\LLL'$
+% % requires a complete global restructuring, then we may say that $\LLL'$
+% % is in some way less expressive than $\LLL$.
 % %
-% \begin{definition}
-%   %
-%   A statically typed programming language $\LLL$ consists of the
-%   following components.
-%   %
-%   \begin{itemize}
-%   \item A signature $\Sigma_T = \{(\ST_i,\ar_i)\}_i$ of \emph{type syntax constructors}.
-%   \item A signature $\Sigma_t = \{(\SC_i,\ar_i)\}_i$ of \emph{term syntax constructors}.
-%   \item A signature $\Sigma_p = \{(\SC_i,
-%   \item A static semantics, which is a function
-%     $typecheck : \Sigma_t \to \B$, which decides whether a
-%     given closed term is well-typed.
-%   \item An operational semantics, which is a partial function
-%     $eval : P \pto R$, where $P$ is the set of well-typed terms, i.e.
+% \begin{definition}[Typeability-preserving macro-expressiveness]
+%   Let both $\LLL = (S, T, E)$ and $\LLL' = (S', T', E')$ be
+%   programming languages such that the syntax constructors
+%   $\SC_1,\dots,\SC_k$ are unique to $\LLL$. If there exists a
+%   translation $\sembr{-} : S \to S'$ on the syntax of $\LLL$ that is
+%   homomorphic on all syntax constructors but $\SC_1,\dots,\SC_k$, such
+%   that for all $A \in \Ty(S)$ and $M \in \Tm(S)$
 %   %
 %   \[
-%       P = \{ t \in \Sigma_t \mid typecheck~t~\text{is true} \},
+%      T(M,A) = T'(\sembr{M},\sembr{A})~\text{and}~
+%      E(M)~\text{holds if and only if}~E'(\sembr{M})~\text{holds},
 %   \]
 %   %
-%     and $R$ is some unspecified set of answers.
-%   \end{itemize}
+%   then we say that $\LLL'$ can \emph{macro-express} the
+%   $\SC_1,\dots,\SC_k$ facilities of $\LLL$.
 % \end{definition}
 % %
+% In general, it is not the case that $\sembr{-}$ preserves types, it is
+% only required to ensure that the translated term is typeable in the
+% target language $\LLL'$.
 
-% An untyped programming language is just a special instance of a
-% statically typed programming language, where the signature of type
-% syntax constructors is a singleton containing a nullary type syntax
-% constructor for the \emph{universal type}, and the function
-% $typecheck$ is a constant function that always returns true.
-
-% A statically polymorphic typed programming language $\LLL$ also
-% includes a set of $\LLL$-kinds of kind syntax constructors as well as
-% a function $kindcheck_\LLL : \LLL\text{-types} \to \B$ which checks
-% whether a given type is well-kinded.
-
-% \begin{definition}
-%   A context free grammar is a quadruple $(N, \Sigma, R, S)$, where
-%   \begin{enumerate}
-%     \item $N$ is a finite set called the nonterminals.
-%     \item $\Sigma$ is a finite set, such that
-%       $\Sigma \cap V = \emptyset$, called the alphabet (or terminals).
-%     \item $R$ is a finite set of rules, each rule is on the form
-%       \[
-%         P ::= (N \cup \Sigma)^\ast, \quad\text{where}~P \in N.
-%       \]
-%     \item $S$ is the initial nonterminal.
-%   \end{enumerate}
+% \begin{definition}[Type-respecting expressiveness]
+%   Let $\LLL = (S,T,E)$ and $\LLL' = (S',T',E')$ be programming
+%   languages and $A$ be a type such that $A \in \Ty(S)$ and
+%   $A \in \Ty(S')$.
 % \end{definition}
 
+% % \dhil{Definition of (typed) programming language, conservative extension, macro-expressiveness~\cite{Felleisen90,Felleisen91}}
 
-% \chapter{State of effectful programming}
-% \label{ch:related-work}
+% % \begin{definition}
+% %   A signature $\Sigma$ is a collection of abstract syntax constructors
+% %   with arities $\{(\SC_i, \ar_i)\}_i$, where $\ST_i$ are syntactic
+% %   entities and $\ar_i$ are natural numbers. Syntax constructors with
+% %   arities $0$, $1$, $2$, and $3$ are referred to as nullary, unary,
+% %   binary, and ternary, respectively.
+% % \end{definition}
 
-% % \section{Type and effect systems}
-% % \section{Monadic programming}
-% \section{Golden age of impurity}
-% \section{Monadic enlightenment}
-% \dhil{Moggi's seminal work applies the notion of monads to effectful
-%   programming by modelling effects as monads. More importantly,
-%   Moggi's work gives a precise characterisation of what's \emph{not}
-%   an effect}
-% \section{Direct-style revolution}
+% % \begin{definition}[Terms in contexts]
+% %   A context $\mathcal{X}$ is set of variables $\{x_1,\dots,x_n\}$. For
+% %   a signature $\Sigma = \{(\SC_i, \ar_i)\}_i$ the $\Sigma$-terms in
+% %   some context $\mathcal{X}$ are generated according to the following
+% %   inductive rules:
+% %   \begin{itemize}
+% %     \item each variable $x_i \in \mathcal{X}$ is a $\Sigma$-term,
+% %     \item if $t_1,\dots,t_{\ar_i}$ are $\Sigma$-terms in context
+% %       $\mathcal{X}$, then $\SC_i(t_1,\dots,t_{\ar_i})$ is
+% %       $\Sigma$-term in context $\mathcal{X}$.
+% %     \end{itemize}
+% %     We write $\mathcal{X} \vdash t$ to indicate that $t$ is a
+% %     $\Sigma$-term in context $\mathcal{X}$. A $\Sigma$-term $t$ is
+% %     said to be closed if $\emptyset \vdash t$, i.e. no variables occur
+% %     in $t$.
+% % \end{definition}
 
-% \subsection{Monadic reflection: best of both worlds}
+% % \begin{definition}
+% %   A $\Sigma$-equation is a pair of terms $t_1,t_2 \in \Sigma$ in
+% %   context $\mathcal{X}$, which we write as
+% %   $\mathcal{X} \vdash t_1 = t_2$.
+% % \end{definition}
+
+% % The notation $\mathcal{X} \vdash t_1 = t_2$ begs to be read as a
+% % logical statement, though, in universal algebra the notation is simply
+% % a syntax. In order to give it a meaning we must first construct a
+% % \emph{model} which interprets the syntax. We shall not delve deeper
+% % here; for our purposes we may think of a $\Sigma$-equation as a
+% % logical statement (the attentive reader may already have realised that .
+
+
+% % The following definition is an adaptation of
+% % \citeauthor{Felleisen90}'s definition of programming language to
+% % define statically typed programming languages~\cite{Felleisen90}.
+% % %
+% % \begin{definition}
+% %   %
+% %   A statically typed programming language $\LLL$ consists of the
+% %   following components.
+% %   %
+% %   \begin{itemize}
+% %   \item A signature $\Sigma_T = \{(\ST_i,\ar_i)\}_i$ of \emph{type syntax constructors}.
+% %   \item A signature $\Sigma_t = \{(\SC_i,\ar_i)\}_i$ of \emph{term syntax constructors}.
+% %   \item A signature $\Sigma_p = \{(\SC_i,
+% %   \item A static semantics, which is a function
+% %     $typecheck : \Sigma_t \to \B$, which decides whether a
+% %     given closed term is well-typed.
+% %   \item An operational semantics, which is a partial function
+% %     $eval : P \pto R$, where $P$ is the set of well-typed terms, i.e.
+% %     %
+% %     \[
+% %       P = \{ t \in \Sigma_t \mid typecheck~t~\text{is true} \},
+% %     \]
+% %     %
+% %     and $R$ is some unspecified set of answers.
+% %   \end{itemize}
+% % \end{definition}
+% % %
+
+% % An untyped programming language is just a special instance of a
+% % statically typed programming language, where the signature of type
+% % syntax constructors is a singleton containing a nullary type syntax
+% % constructor for the \emph{universal type}, and the function
+% % $typecheck$ is a constant function that always returns true.
+
+% % A statically polymorphic typed programming language $\LLL$ also
+% % includes a set of $\LLL$-kinds of kind syntax constructors as well as
+% % a function $kindcheck_\LLL : \LLL\text{-types} \to \B$ which checks
+% % whether a given type is well-kinded.
+
+% % \begin{definition}
+% %   A context free grammar is a quadruple $(N, \Sigma, R, S)$, where
+% %   \begin{enumerate}
+% %     \item $N$ is a finite set called the nonterminals.
+% %     \item $\Sigma$ is a finite set, such that
+% %       $\Sigma \cap V = \emptyset$, called the alphabet (or terminals).
+% %     \item $R$ is a finite set of rules, each rule is on the form
+% %       \[
+% %         P ::= (N \cup \Sigma)^\ast, \quad\text{where}~P \in N.
+% %       \]
+% %     \item $S$ is the initial nonterminal.
+% %   \end{enumerate}
+% % \end{definition}
+
+
+% % \chapter{State of effectful programming}
+% % \label{ch:related-work}
+
+% % % \section{Type and effect systems}
+% % % \section{Monadic programming}
+% % \section{Golden age of impurity}
+% % \section{Monadic enlightenment}
+% % \dhil{Moggi's seminal work applies the notion of monads to effectful
+% %   programming by modelling effects as monads. More importantly,
+% %   Moggi's work gives a precise characterisation of what's \emph{not}
+% %   an effect}
+% % \section{Direct-style revolution}
+
+% % \subsection{Monadic reflection: best of both worlds}
 
 \chapter{Continuations}
 \label{ch:continuations}
@@ -3687,14 +3724,22 @@ is same as $\FelleisenF$. However, the presentation here is close to
 actual implementations of $\Control$.
 
 The static semantics of control and prompt were absent in
-\citeauthor{Felleisen88}'s original treatment.
+\citeauthor{Felleisen88}'s original treatment. Later,
+\citet{KameyamaY08} have given a polymorphic type system with answer
+type modifications for control and prompt (we will discuss answer type
+modification when discussing shift/reset). It is also worth mentioning
+that \citet{DybvigJS07} present a typed embedding of control and
+prompts in Haskell (actually, they present an entire general monadic
+framework for implementing control operators based on the idea of
+\emph{multi-prompts}, which are a slight generalisation of prompts ---
+we will revisit multi-prompts when we discuss splitter and cupto).
 %
-\dhil{Mention Yonezawa and Kameyama's type system.}
-%
-\citet{DybvigJS07} gave a typed embedding of multi-prompts in
-Haskell. In the multi-prompt setting the prompts are named and an
-instance of $\Control$ is indexed by the prompt name of its designated
-delimiter.
+% \dhil{Mention Yonezawa and Kameyama's type system.}
+% %
+% \citet{DybvigJS07} gave a typed embedding of multi-prompts in
+% Haskell. In the multi-prompt setting the prompts are named and an
+% instance of $\Control$ is indexed by the prompt name of its designated
+% delimiter.
 
 % Typing them, particularly using a simple type system,
 % affect their expressivity, because the type of the continuation object
@@ -3824,12 +3869,37 @@ second application of $\Control$ captures the remainder of the
 computation of to $\Prompt$. However, the captured context gets
 discarded, because the continuation $k'$ is never invoked.
 %
-\dhil{Mention control0/prompt0 and the control hierarchy}
+
+A slight variation on control and prompt is $\Controlz$ and
+$\Promptz$~\cite{Shan04}. The main difference is that $\Controlz$
+removes its corresponding prompt, i.e.
+%
+\begin{reductions}
+  % \slab{Value} &
+  %    \Prompt~V &\reducesto& V\\
+  \slab{Capture_0} &
+     \Promptz~\EC[\Controlz~k.M] &\reducesto& M[\qq{\cont_{\EC}}/k], \text{ where $\EC$ contains no \Promptz}\\
+  % \slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
+\end{reductions}
+%
+Higher-order programming with control and prompt (and delimited
+control in general) is fragile, because the body of a higher-order
+function may inadvertently trap instances of control in its functional
+arguments.
+%
+This observation led \citet{SitaramF90} to define an indexed family of
+control and prompt pairs such that instances of control and prompt can
+be layered on top of one another. The idea is that the index on each
+pair denotes their level $i$ such that $\Control^i$ matches
+$\Prompt^i$ and may capture any other instances of $\Prompt^j$ where
+$j < i$.
+% \dhil{Mention control0/prompt0 and
+%   the control hierarchy}
 
 \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
+reset appeared in \citeauthor{DanvyF90}'s seminal work on abstracting
 control the following year~\cite{DanvyF90}.
 %
 Shift and reset differ from control and prompt in that the contexts
@@ -3897,24 +3967,24 @@ substructural type system with answer type modification, whilst
 language with answer type modification into a system without using
 typed multi-prompts.
 
-Differences between shift/reset and control/prompt manifests in the
+Differences between shift/reset and control/prompt manifest in the
 dynamic semantics as well.
 %
 \begin{reductions}
   \slab{Value}    & \reset{V}               &\reducesto& V\\
-  \slab{Capture}  & \reset{\EC[\shift\;k.M]} &\reducesto& \reset{M[\qq{\cont_{\EC}}/k]}, \text { where $\EC$ contains no $\reset{-}$}\\
+  \slab{Capture}  & \reset{\EC[\shift\;k.M]} &\reducesto& \reset{M[\qq{\cont_{\reset{\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]}\\
+  \slab{Resume}   & \Continue~\cont_{\reset{\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.
+The key difference between \citeauthor{Felleisen88}'s control/prompt
+and shift/reset is that the $\slab{Capture}$ rule for the latter
+includes a copy of the delimiter in the reified continuation. This
+delimiter gets installed along with the captured context $\EC$ when
+the continuation object is resumed. 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'.4)}\\
@@ -3935,20 +4005,70 @@ previous 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
+differences. \citet{Shan04} answered this question demonstrating 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}.
 %
+
+As with control and prompt there exist various variation of shift and
+reset. \citet{DanvyF89} also considered $\shiftz$ and
+$\resetz{-}$. The operational difference between $\shiftz$/$\resetz{-}$
+and $\shift$/$\reset{-}$ manifests in the capture rule.
 %
-\dhil{Maybe mention the implication is that control/prompt has CPS semantics.}
-\dhil{Mention shift0/reset0, dollar0\dots}
+\begin{reductions}
+  \slab{Capture_0}  & \resetz{\EC[\shiftz\,k.M]} &\reducesto& M[\qq{\cont_{\resetz{\EC}}}/k], \text { where $\EC$ contains no $\resetz{-}$}\\
+\end{reductions}
+%
+The control reifier captures the continuation up to and including its
+delimiter, however, unlike $\shift$, it removes the control delimiter
+from the current evaluation context. Thus $\shiftz$/$\resetz{-}$ are
+`dynamic' variations on $\shift$/$\reset{-}$. \citet{MaterzokB12}
+introduced $\dollarz{-}{-}$ (pronounced ``dollar0'') as an
+alternative control delimiter for $\shiftz$.
+\begin{reductions}
+  \slab{Value_{\$_0}} & \dollarz{x.N}{V}  &\reducesto& N[V/x]\\
+  \slab{Capture_{\$_0}}  & \dollarz{x.N}{\EC[\shiftz\,k.M]} &\reducesto& M[\qq{\cont_{(\dollarzh{x.N}{\EC})}}/k],\\
+  &&&\quad\text{where $\EC$ contains no $\reset{-\mid-}$}\\
+  \slab{Resume_{\$_0}}   & \Continue~\cont_{(\dollarz{x.N}{\EC})}~V &\reducesto& \dollarz{x.N}{\EC[V]}\\
+\end{reductions}
+%
+The intuition here is that $\dollarz{x.N}{M}$ evaluates $M$ to some
+value $V$ in a fresh context, and then continues as $N$ with $x$ bound
+to $V$. Thus it builds in a form of ``success continuation'' that
+makes it possible to post-process the result of a reset0 term. In
+fact, reset0 is macro-expressible in terms of
+dollar0~\cite{MaterzokB12}.
+%
+\[
+ \sembr{\resetz{M}} \defas \dollarz{x.x}{\sembr{M}}\\
+\]
+%
+By taking the success continuation to be the identity function dollar0
+becomes operationally equivalent to reset0. As it turns out reset0 and
+shift0 (together) can macro-express dollar0~\cite{MaterzokB12}.
+%
+\[
+ \sembr{\dollarz{x.N}{M}} \defas (\lambda k.\resetz{(\lambda x.\shiftz~z.k~x)\,\sembr{M}})\,(\lambda x.\sembr{N})
+\]
+%
+This translation is a little more involved. The basic idea is to first
+explicit pass in the success continuation, then evaluate $M$ under a
+reset to yield value which gets bound to $x$, and then subsequently
+uninstall the reset by invoking $\shiftz$ and throwing away the
+captured continuation, afterwards we invoke the success continuation
+with the value $x$.
+
+% Even though the two constructs are equi-expressive (in the sense of macro-expressiveness) there are good reason for preferring dollar0 over reset0 Since the two constructs are equi-expressive, the curious reader might
+% wonder why \citet{MaterzokB12} were
+
+% \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]\\
@@ -3957,18 +4077,18 @@ and state~\cite{Filinski94}.
 %
 
 \paragraph{\citeauthor{QueinnecS91}'s splitter} The `splitter' control
-operator reconciles abortive undelimited control and composable
-delimited control. It was introduced by \citet{QueinnecS91} in
-1991. The name `splitter' is derived from it operational behaviour, as
-an application of `splitter' marks evaluation context in order for it
-to be split into two parts, where the context outside the mark
-represents the rest of computation, and the context inside the mark
-may be reified into a delimited continuation. The operator supports
-two operations `abort' and `calldc' to control the splitting of
-evaluation contexts. The former has the effect of escaping to the
-outer context, whilst the latter reifies the inner context as a
-delimited continuation (the operation name is short for ``call with
-delimited continuation'').
+operator reconciles abortive continuations and composable
+continuations. It was introduced by \citet{QueinnecS91} in 1991. The
+name `splitter' is derived from it operational behaviour, as an
+application of `splitter' marks evaluation context in order for it to
+be split into two parts, where the context outside the mark represents
+the rest of computation, and the context inside the mark may be
+reified into a delimited continuation. The operator supports two
+operations `abort' and `calldc' to control the splitting of evaluation
+contexts. The former has the effect of escaping to the outer context,
+whilst the latter reifies the inner context as a delimited
+continuation (the operation name is short for ``call with delimited
+continuation'').
 
 Splitter and the two operations abort and calldc are value forms.
 %
@@ -3976,7 +4096,7 @@ Splitter and the two operations abort and calldc are value forms.
   V,W ::= \cdots \mid \splitter \mid \abort \mid \calldc
 \]
 %
-In their treatise of splitter, \citeauthor{QueinnecS91} gave three
+In their treatment of splitter, \citeauthor{QueinnecS91} gave three
 different presentations of splitter. The presentation that I have
 opted for here is close to their second presentation, which is in
 terms of multi-prompt continuations. This variation of splitter admits
@@ -4042,8 +4162,8 @@ track of which prompt names have already been allocated.
 \begin{reductions}
   \slab{AppSplitter} & \splitter~V,\rho &\reducesto& \Prompt_p~V\,p,\rho \uplus \{p\}\\
   \slab{Value}    & \Prompt_p~V,\rho &\reducesto& V,\rho\\
-  \slab{Abort}    & \Prompt_p~\EC[\abort~\Record{p;V}],\rho &\reducesto& V\,\Unit,\rho,\quad \text{where $\EC$ contains no $\Prompt_p$}\\
-  \slab{Capture}  & \Prompt_p~\EC[\calldc~V] &\reducesto& V~\qq{\cont_{\EC}},\rho\\
+  \slab{Abort}    & \Prompt_p~\EC[\abort\,\Record{p;V}],\rho &\reducesto& V\,\Unit,\rho\\%, \quad \text{where $\EC$ contains no $\Prompt_p$}\\
+  \slab{Capture}  & \Prompt_p~\EC[\calldc\,\Record{p;V}] &\reducesto& V~\qq{\cont_{\EC}},\rho\\
   \slab{Resume}   & \Continue~\cont_{\EC}~V,\rho &\reducesto& \EC[V],\rho
 \end{reductions}
 %
@@ -4064,13 +4184,58 @@ operation the prompt is removed. % Thus, $\calldc$ behaves as a
 % delimited variation of $\Callcc$.
 %
 
-It is clear by the prompt semantics that invocation of either $\abort$
-and $\calldc$ is only well-defined within the dynamic extent of
-$\splitter$. Since the prompt is eliminated after use of either
+It is clear by the prompt semantics that an invocation of either
+$\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$.
 %
-\dhil{Show an example}
+\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\\
+  \reducesto& \reason{\slab{AppSplitter}}\\
+  &2 + \Prompt_p~2 + \splitter\,(\lambda p'.3 + \calldc\,\Record{p;\lambda k. k~0 + \abort\,\Record{p';\lambda\Unit.k~1}}), \{p\}\\
+  \reducesto& \reason{\slab{AppSplitter}}\\
+  &2 + \Prompt_p~2 + \Prompt_{p'}~3 + \calldc\,\Record{p;\lambda k. k~0 + \abort\,\Record{p';\lambda\Unit.k~1}}, \{p,p'\}\\
+  \reducesto& \reason{\slab{Capture} $\EC = 2 + \Prompt_{p'}~3 + [\,]$}\\
+  &2 + k~0 + \abort\,\Record{p';\lambda\Unit.k~1}, \{p,p'\}\\
+  \reducesto& \reason{\slab{Resume} $\EC$ with $0$}\\
+  &2 + 2 + \Prompt_{p'}~3 + \abort\,\Record{p';\lambda\Unit.\qq{\cont_{\EC}}\,1}, \{p,p'\}\\
+  \reducesto^+& \reason{\slab{Abort}}\\
+  & 4 + \qq{\cont_{\EC}}\,1, \{p,p'\}\\
+  \reducesto& \reason{\slab{Resume} $\EC$ with $1$}\\
+  & 4 + 2 + \Prompt_{p'}~3 + 1, \{p,p'\}\\
+  \reducesto^+& \reason{\slab{Value}}\\
+  & 6 + 4, \{p,p'\} \reducesto 10, \{p,p'\}
+\end{derivation}
+%
+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.
+% \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}}\\
+%   &1 + \Prompt_p~2 + \splitter\,(\lambda p'.3 + \calldc\,\Record{p;\lambda k.k~1 + \calldc\,\Record{p';\lambda k'. k\,(k'~1)}})), \{p\}\\
+%   \reducesto& \reason{\slab{AppSplitter}}\\
+%   &1 + \Prompt_p~2 + \Prompt_{p'} 3 + \calldc\,\Record{p';\lambda k.k~0 + \calldc\,\Record{p';\lambda k'. k\,(k'~1)}}, \{p,p'\}\\
+%   \reducesto& \reason{\slab{Capture} $\EC = 2 + \Prompt_{p'}~3 + [\,]$}, \{p,p'\}\\
+%   &1 + ((\lambda k.k~0 + \calldc\,\Record{p';\lambda k'. k\,(k'~1)})\,\qq{\cont_\EC}),\{p,p'\}\\
+%   \reducesto^+& \reason{\slab{Resume} $\EC$ with $0$}\\
+%   &1 + 2 + \Prompt_{p'}~3 + 0 + \calldc\,\Record{p';\lambda k'. \qq{\cont_\EC}\,(k'~1)}\\
+%   \reducesto^+& \reason{\slab{Capture} $\EC' = 3 + [\,]$}\\
+%   &3 + (\lambda k'. \qq{\cont_\EC}\,(k'~1)\,\qq{\cont_{\EC'}})\\
+%   \reducesto^+& \reason{\slab{Resume} $\EC'$ with $1$}\\
+%   &3 + \qq{\cont_\EC}\,(3 + 1)\\
+%   \reducesto^+& \reason{\slab{Resume} $\EC$ with $4$}\\
+%   &3 + 2 + \Prompt_{p'}~3 + 4\\
+%   \reducesto^+& \reason{\slab{Value}}\\
+%   &5 + 7 \reducesto 13
+% \end{derivation}
+%
+
 % \begin{reductions}
 %   \slab{Value}   & \splitter~abort~calldc.V &\reducesto& V\\
 %   \slab{Throw}   & \splitter~abort~calldc.\EC[\,abort~V] &\reducesto& V~\Unit\\
@@ -4487,7 +4652,7 @@ The $\slab{Capture}$ reifies the continuation up to the handler, and
 thus the $\slab{Resume}$ rule can only reinstate the captured
 continuation without the handler.
 %
-\dhil{Revisit the toss example with shallow handlers}
+%\dhil{Revisit the toss example with shallow handlers}
 % \begin{reductions}
 %   \slab{Capture}  & \Handle\;\EC[\Do\;\ell~V] \;\With\; H &\reducesto& M[V/p,\qq{\cont_{\EC}}/k],\\
 %   \multicolumn{4}{l}{\hfill\bl\text{where $\ell$ is not handled in $\EC$}\\\text{and }\{\ell~p~k \mapsto M\} \in H\el}\\
@@ -6002,7 +6167,7 @@ semantics of \BCalc{}. In this section, we state and prove some
 customary metatheoretic properties about \BCalc{}.
 %
 
-We begin by showing that substitutions preserve typability.
+We begin by showing that substitutions preserve typeability.
 %
 \begin{lemma}[Preservation of typing under substitution]\label{lem:base-language-subst}
   Let $\sigma$ be any type substitution and $V \in \ValCat$ be any
@@ -14355,17 +14520,18 @@ setting.
 %
 
 We will restrict our attention to the calculi $\HCalc$, $\SCalc$, and
-$\HPCalc$ and use the notion of \emph{typability-preserving
+$\HPCalc$ and use the notion of \emph{typeability-preserving
   macro-expressiveness} to determine whether handlers are
-interdefinable. In our particular setting, typability-preserving
-macro-expressiveness asks whether there exists a \emph{local}
-transformation that can transform one kind of handler into another
-kind of handler, whilst preserving typability in the image of the
-transformation. By mandating that the transform is local we rule out
-the possibility of rewriting the entire program in, say, CPS notation
-to implement deep and shallow handlers as in Chapter~\ref{ch:cps}.
+interdefinable~\cite{ForsterKLP19}. In our particular setting,
+typeability-preserving macro-expressiveness asks whether there exists
+a \emph{local} transformation that can transform one kind of handler
+into another kind of handler, whilst preserving typeability in the
+image of the transformation. By mandating that the transform is local
+we rule out the possibility of rewriting the entire program in, say,
+CPS notation to implement deep and shallow handlers as in
+Chapter~\ref{ch:cps}.
 %
-In this chapter we use the notion of typability-preserving
+In this chapter we use the notion of typeability-preserving
 macro-expressiveness to show that shallow handlers and general
 recursion can simulate deep handlers up to congruence, and that deep
 handlers can simulate shallow handlers up to administrative
@@ -14464,7 +14630,7 @@ The deep semantics are simulated by generating the name $env$ for the
 shallow handlers and recursively apply the handler under the modified
 resumption.
 
-The translation commutes with substitution and preserves typability.
+The translation commutes with substitution and preserves typeability.
 %
 \begin{lemma}\label{lem:dstrans-subst}
   Let $\sigma$ denote a substitution. The translation $\dstrans{-}$
@@ -14658,13 +14824,13 @@ $\BigO(1)$ time in the source, but in the image it takes $\BigO(k)$
 time.
 %
 Thus this translation is more of theoretical significance than
-practical interest. It also demonstrates that typability-preserving
+practical interest. It also demonstrates that typeability-preserving
 macro-expressiveness is rather coarse-grained notion of
 expressiveness, as it blindly considers whether some construct is
 computable using another construct without considering the
 computational cost.
 
-The translation commutes with substitution and preserves typability.
+The translation commutes with substitution and preserves typeability.
 %
 \begin{lemma}\label{lem:sdtrans-subst}
   Let $\sigma$ denote a substitution. The translation $\sdtrans{-}$
@@ -14695,7 +14861,7 @@ If $\Delta; \Gamma \vdash M : C$ then $\sdtrans{\Delta};
 \newcommand{\approxa}{\gtrsim}
 
 As with the implementation of deep handlers as shallow handlers, the
-implementation is again given by a typability-preserving local
+implementation is again given by a typeability-preserving local
 translation. However, this time the administrative overhead is more
 significant. Reduction up to congruence is insufficient and we require
 a more semantic notion of administrative reduction.
@@ -15232,7 +15398,7 @@ handler into an ordinary deep handler that makes use of the
 parameter-passing idiom to maintain the state of the handled
 computation~\cite{Pretnar15}.
 
-The translation commutes with substitution and preserves typability.
+The translation commutes with substitution and preserves typeability.
 %
 \begin{lemma}\label{lem:pd-subst}
   Let $\sigma$ denote a substitution. The translation $\PD{-}$
@@ -15338,7 +15504,7 @@ myself on the inherited efficiency of effect handlers
 (c.f. Chapter~\ref{ch:handlers-efficiency}) and \citet{ForsterKLP17}, who
 investigate various relationships between effect handlers, delimited
 control in the form of shift/reset, and monadic reflection using the
-notions of typability-preserving macro-expressiveness and untyped
+notions of typeability-preserving macro-expressiveness and untyped
 macro-expressiveness~\cite{ForsterKLP17,ForsterKLP19}. They show that
 in an untyped setting all three are interdefinable, whereas in a
 simply typed setting effect handlers cannot macro-express
@@ -15363,7 +15529,7 @@ the captured context and continuation invocation context to coincide.
 % \label{ch:expressiveness}
 % \section{Notions of expressiveness}
 % Felleisen's macro-expressiveness, Longley's type-respecting
-% expressiveness, Kammar's typability-preserving expressiveness.
+% expressiveness, Kammar's typeability-preserving expressiveness.
 
 \chapter{Asymptotic speedup with effect handlers}
 \label{ch:handlers-efficiency}