Fix bibliography: add missing year

This commit fixes a typo in the type signature of `init` (thanks to
Ramsay Carslaw for spotting it). This commit also structures the last
sentence of Section 2.7 to read slightly better.

README.md

@@ -116,4 +116,5 @@ I submitted my thesis on May 30, 2021. It was examined on August 13,
 2021, where I received pass with minor corrections. The revised thesis
 was submitted on December 22, 2021. It was approved on March
 14, 2022. The final revision was submitted on March 23, 2022. I
-received my PhD award letter on March 24, 2022.
+received my PhD award letter on March 24, 2022. My graduation 
+ceremony took place in McEwan Hall on July 11, 2022.

thesis.bib

@@ -2401,7 +2401,8 @@
   author    = {Nikolaos S. Papspyrou},
   title     = {A resumption monad transformer and its applications in the semantics of concurrency},
   booktitle = {Proceedings of the 3rd Panhellenic Logic Symposium},
-  address   = {Anogia, Greece}
+  address   = {Anogia, Greece},
+  year      = 2001,
 }
 
 @inproceedings{Harrison06,

thesis.tex

@@ -167,7 +167,7 @@
   %
   Effect handlers provide a particularly structured approach to
   programming with first-class control by naming control reifying
-  operations and separating from their handling.
+  operations and separating them from their handling.
 
   This thesis is composed of three strands of work in which I develop
   operational foundations for programming and implementing effect
@@ -5446,7 +5446,7 @@ created by the operating system.
 %
 \[
   \bl
-    \init : (\Unit \to \alpha \eff \varepsilon) \to \alpha \eff \{\Co;\varepsilon\}\\
+    \init : (\UnitType \to \UnitType \eff \varepsilon) \to \UnitType \eff \{\Co;\varepsilon\}\\
     \init~main \defas
       \bl
         \Let\;pid \revto \Do\;\UFork~\Unit\;\In\\
@@ -5535,10 +5535,11 @@ $\Fork : \UnitType \opto \Bool$, by $\timesharee$, which handles the
 more general operation $\UFork : \UnitType \opto \Int$. In practice,
 we may be unable to dispense of the old interface so easily, meaning
 we have to retain support for, say, legacy reasons. As we have seen
-previously we can an operation in terms of another operation. Thus to
-retain support for $\Fork$ we simply have to insert a handler under
-$\timesharee$ which interprets $\Fork$ in terms of $\UFork$. The
-operation case of this handler would be akin to the following.
+previously we can interpret an operation in terms of another
+operation. Thus to retain support for $\Fork$ we simply have to insert
+a handler under $\timesharee$ which interprets $\Fork$ in terms of
+$\UFork$. The operation case of this handler would be akin to the
+following.
 %
 \[
   \OpCase{\Fork}{\Unit}{resume} \mapsto
@@ -5552,7 +5553,7 @@ The interpretation of $\Fork$ inspects the process identifier returned
 by the $\UFork$ to determine the role of the current process in the
 parent-child relationship. If the identifier is nonzero, then the
 process is a parent, hence $\Fork$ should return $\True$ to its
-caller. Otherwise it should return $\False$. This preserves the
+caller, and otherwise it should return $\False$, thus preserving the
 functionality of the legacy code.
 
 \section{Related work}
@@ -6547,9 +6548,9 @@ Computations
 % Let
   \inferrule*[Lab=\tylab{Let}]
     {\typc{\Delta;\Gamma}{M : A}{E} \\
-     \typ{\Delta;\Gamma, x : A}{N : C}
+     \typc{\Delta;\Gamma, x : A}{N : B}{E}
     }
-    {\typ{\Delta;\Gamma}{\Let \; x \revto M\; \In \; N : C}}
+    {\typc{\Delta;\Gamma}{\Let \; x \revto M\; \In \; N : B}{E}}
 \end{mathpar}
 \caption{Typing rules}
 \label{fig:base-language-type-rules}
@@ -6673,7 +6674,7 @@ that the binder $x : A$.
   \EC[M] &\reducesto& \EC[N], \hfill\quad \text{if } M \reducesto N \\
 \end{reductions}
 \begin{syntax}
-\slab{Evaluation contexts} &  \mathcal{E} \in \EvalCat &::=& [~] \mid \Let \; x \revto \mathcal{E} \; \In \; N
+\slab{Evaluation~contexts} &  \mathcal{E} \in \EvalCat &::=& [~] \mid \Let \; x \revto \mathcal{E} \; \In \; N
 \end{syntax}
 %
 %\dhil{Describe evaluation contexts as functions: decompose and plug.}
@@ -17244,7 +17245,7 @@ They identify four variations.
   delimiter in the reified context, but discards the original
   instance, i.e.
   \[
-    \Delim{\EC[\CC~k.M]} \reducesto M[\cont_{\EC}/k]
+    \Delim{\EC[\CC~k.M]} \reducesto M[\cont_{\Delim{\EC}}/k]
   \]
 \item[\CCmm] The control reifier reifies the context up to, but not
   including, the delimiter and subsequently discards the delimiter, i.e.
@@ -17486,21 +17487,22 @@ the desire to provide a `functional' equivalent of jumps as provided
 by the infamous goto in imperative programming.
 %
 
-In 1965 Peter \citeauthor{Landin65} unveiled \emph{first} first-class
-control operator: the J
+In 1965 Peter \citeauthor{Landin65} unveiled the \emph{first}
+first-class control operator: the J
 operator~\cite{Landin65,Landin65a,Landin98}. Later in 1972 influenced
 by \citeauthor{Landin65}'s J operator John \citeauthor{Reynolds98a}
 designed the escape operator~\cite{Reynolds98a}. Influenced by escape,
 \citeauthor{SussmanS75} designed, implemented, and standardised the
 catch operator in Scheme in 1975. A while thereafter the perhaps most
-famous undelimited control operator appeared: callcc. It initially
-designed in 1982 and was standardised in 1985 as a core feature of
-Scheme. Later another batch of control operators based on callcc
-appeared. A common characteristic of the early control operators is
-that their capture mechanisms were abortive and their captured
-continuations were abortive, save for one, namely,
-\citeauthor{Felleisen88}'s F operator. Later a non-abortive and
-composable variant of callcc appeared. Moreover, every operator,
+famous undelimited control operator appeared: callcc. It was designed
+in 1982 and standardised in 1985 as a core feature of
+Scheme. Following on from callcc a wide range of different control
+operators was designed. A common characteristic of the early control
+operators is that their capture mechanisms are abortive and their
+captured continuations are abortive, save for one, namely,
+\citeauthor{Felleisen88}'s F operator. Though, it is worth remarking
+that \citet{FlattYFF07} devised a non-abortive and composable variant
+of callcc. Another common characteristic is that every operator,
 except for \citeauthor{Landin98}'s J operator, capture the current
 continuation.
 
@@ -17832,7 +17834,7 @@ follows.
 \end{reductions}
 %
 Their capture rules are identical. Both operators abort the current
-continuation upon capture. This is what set $\FelleisenF$ apart from
+continuation upon capture. This is what sets $\FelleisenF$ apart from
 the other composable control operator $\Callcomc$.
 %
 The resume rules of $\FelleisenC$ and $\FelleisenF$ show the
@@ -19022,7 +19024,7 @@ computation $M$ with handler $H$.
        \{\ell_i : A_i \opto B_i\}_i \in \Sigma \\
        H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{k_i} \mapsto N_i \}_i \\
        \el}\\\\
-       \typ{\Gamma, x : A;\Sigma}{M : D}\\\\
+       \typ{\Gamma, x : C;\Sigma}{M : D}\\\\
        [\typ{\Gamma,p_i : A_i, k_i : B_i \to D;\Sigma}{N_i : D}]_i
     }
     {\typ{\Gamma;\Sigma}{H : C \Harrow D}}
@@ -19210,7 +19212,7 @@ handler definitions are identical, however, their typing differ.
        \{\ell_i : A_i \opto B_i\}_i \in \Sigma \\
        H = \{\Return\;x \mapsto M\} \uplus \{ \OpCase{\ell_i}{p_i}{k_i} \mapsto N_i \}_i \\
        \el}\\\\
-       \typ{\Gamma, x : A;\Sigma}{M : D}\\\\
+       \typ{\Gamma, x : C;\Sigma}{M : D}\\\\
        [\typ{\Gamma,p_i : A_i, k_i : B_i \to C;\Sigma}{N_i : D}]_i
     }
     {\typ{\Gamma;\Sigma}{H : C \Harrow D}}
@@ -19735,7 +19737,7 @@ overhead, although, techniques such as just-in-time compilation can be
 utilised to reduce this overhead.
 
 Continuation passing style (CPS) is a canonical implementation
-strategy for continuations --- the word `continuation' even feature in
+strategy for continuations --- the word `continuation' even features in
 its name.
 %
 CPS is a particular idiomatic notation for programs, where every
@@ -19769,9 +19771,9 @@ equations.
 However, the first equation is derivable from the second and third
 equations. I first learned this from Paul{-}Andr{\'{e}} Melli{\`{e}}s
 during Shonan Seminar No.103 \emph{Semantics of Effects, Resources,
-  and Applications}. I have been unable to find a proof of this fact
-in the literature, though, \citeauthor{Mellies14} does have published
-paper, which only states the three necessary
+and Applications}. I have been unable to find a proof of this fact in
+the literature, though, \citeauthor{Mellies14} does have a published
+paper, which states only the three necessary
 equations~\cite{Mellies14}.
 %
 Therefore I include a proof of this fact here (thanks to Sam Lindley
@@ -21514,7 +21516,7 @@ $\BergerCount$ program alluded to in Section~\ref{sec:pure-counting},
 in order to fill out our overall picture of the relationship between
 language expressivity and potential program efficiency.
 
-\paragraph{Relation to prior work} This appendix imported from
+\paragraph{Relation to prior work} This appendix is imported from
 Appendix D of \citet{HillerstromLL20a}. The code snippets in this
 appendix are based on an implementation of Berger count in SML/NJ
 written by John Longley. I have transcribed the code snippets, and in