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

@@ -1,16 +1,13 @@
 # Foundations for programming and implementing effect handlers
 
-**NOTE** I have made a draft copy of the dissertation available in
-this repository. I ask that you **do not** link to or distribute the
-draft anywhere, because I will delete the file once the final revision
-has been submitted after the viva. I will make the final revision
-publicly available at a stable link.
+A copy of my dissertation can be [downloaded via my
+website](https://dhil.net/research/papers/thesis.pdf).
 
----
+----
 
-Submitted May 30, 2021. Viva August 13, 2021.
+Submitted on May 30, 2021. Examined on August 13, 2021.
 
-The board of examiners consists of
+The board of examiners were
 
 * [Andrew Kennedy](https://github.com/andrewjkennedy) (Facebook London)
 * [Edwin Brady](https://www.type-driven.org.uk/edwinb/) (University of St Andrews)
@@ -30,73 +27,72 @@ The dissertation is structured as follows.
    and contributions of the dissertation, and discusses some related
    work.
 
-### Background
-
- * Chapter 2 defines some basic mathematical notation and
-constructions that are they pervasively throughout this dissertation.
-
- * Chapter 3 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.
-
 ### Programming
 
- * Chapter 4 introduces a polymorphic fine-grain call-by-value core
-calculus, λ<sub>b</sub>, which makes key use of Remy-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 2 illustrates effect handler oriented programming by
+   example by implementing a small operating system dubbed Tiny UNIX,
+   which captures some essential traits of Ritchie and Thompson's
+   UNIX. The implementation starts with a basic notion of file i/o,
+   and then, it evolves into a feature-rich operating system with full
+   file i/o, multiple user environments, multi-tasking, and more, by
+   composing ever more effect handlers.
 
- * Chapter 5 presents three extensions of λ<sub>b</sub>,
-which are λ<sub>h</sub> that adds deep handlers, λ<sup>†</sup> that adds shallow
-handlers, and λ<sup>‡</sup> 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 Tiny UNIX based on Ritchie and Thompson's original
-UNIX.
+ * Chapter 3 introduces a polymorphic fine-grain call-by-value core
+   calculus, λ<sub>b</sub>, which makes key use of Rémy-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. The chapter also
+   presents three extensions of λ<sub>b</sub>, which are λ<sub>h</sub>
+   that adds deep handlers, λ<sup>†</sup> that adds shallow handlers,
+   and λ<sup>‡</sup> that adds parameterised handlers.
 
 ### Implementation
 
- * Chapter 6 develops a higher-order continuation passing
-style translation for effect handlers through a series of step-wise
+ * Chapter 4 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 λ<sub>b</sub>. Each refinement slightly modifies the notion
-of continuation employed by the translation. The development
-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.
+   translation for λ<sub>b</sub>. Each refinement slightly modifies
+   the notion of continuation employed by the translation. The
+   development 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 7 demonstrates an application of generalised continuations
+ * Chapter 5 demonstrates an application of generalised continuations
    to abstract machine as we plug generalised continuations into
    Felleisen and Friedman's CEK machine to obtain an adequate abstract
-runtime with simultaneous support for deep, shallow, and parameterised
-handlers.
+   runtime with simultaneous support for deep, shallow, and
+   parameterised handlers.
 
 ### Expressiveness
- * Chapter 8 shows that deep, shallow, and parameterised notions of
+
+ * Chapter 6 shows that deep, shallow, and parameterised notions of
    handlers can simulate one another up to specific notions of
    administrative reduction.
 
- * Chapter 9 studies the fundamental efficiency of effect handlers. In
+ * Chapter 7 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 *generic count* problem using
-a pure PCF-like base language λ<sub>b</sub><sup>→</sup> (a simply typed variation of
-λ<sub>b</sub>) and its extension with effect handlers λ<sub>h</sub><sup>→</sup>.  We
-show that λ<sub>h</sub><sup>→</sup> admits an asymptotically more efficient
-implementation of generic count than any λ<sub>b</sub><sup>→</sup> implementation.
+   functions. Specifically, we consider the *generic count* problem
+   using a pure PCF-like base language λ<sub>b</sub><sup>→</sup> (a
+   simply typed variation of λ<sub>b</sub>) and its extension with
+   effect handlers λ<sub>h</sub><sup>→</sup>.  We show that
+   λ<sub>h</sub><sup>→</sup> admits an asymptotically more efficient
+   implementation of generic count than any λ<sub>b</sub><sup>→</sup>
+   implementation.
 
 ### Conclusions
-  * Chapter 10 concludes and discusses future work.
+  * Chapter 8 concludes and discusses future work.
 
 ### Appendices
-  * Appendix A contains a proof that shows the `Get-get` equation for
+
+ * Appendix A contains 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.
+ * Appendix B contains a proof that shows the `Get-get` equation for
    state is redundant.
-  * Appendix B contains the proof details for the higher-order
-    uncurried CPS translation for deep and shallow handlers.
  * Appendix C contains the proof details and gadgetry for the
    complexity of the effectful generic count program.
  * Appendix D provides a sample implementation of the Berger count
@@ -114,3 +110,11 @@ e.g.
 $ make
 ```
 
+## Timeline
+
+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. My graduation 
+ceremony took place in McEwan Hall on July 11, 2022.

thesis.bib

@@ -1258,7 +1258,7 @@
 
 @techreport{Remy93,
   title = {{Syntactic theories and the algebra of record terms}},
-  author = {Didier Remy},
+  author = {Didier R\'{e}my},
   number = {RR-1869},
   institution = {{INRIA}},
   year = {1993},
@@ -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
@@ -313,32 +313,33 @@
   about my work.
   %
   Thirdly, I want to thank my academic brother Simon Fowler, who has
-  always been a good friend and a pillar of inspiration. Regardless of
-  academic triumphs and failures, we have always had fun.
+  always been a good and inspirational friend. Regardless of academic
+  triumphs and failures, we have always had fun.
 
   I am extremely grateful to KC Sivaramakrishnan, who took a genuine
   interest in my research early on and invited me to come spend some
   time at OCaml Labs in Cambridge. My initial visit to Cambridge
   sparked the beginning of a long-standing and productive
-  collaboration. Also, thanks to Gemma Gordon, who I had the pleasure
-  of sharing an office with during one of my stints at OCaml Labs.
+  collaboration. Also, thanks to Gemma Gordon, who I have had the
+  pleasure of sharing an office with during one of my stints at OCaml
+  Labs.
 
   I have been fortunate to work with Robert Atkey, who has been a
   continuous source of inspiration and interesting research ideas. Our
   work is clearly reflected in this dissertation.
   %
-  I also want to thank my other collaborators: Andreas Rossberg, Anil
-  Madhavapeddy, Leo White, Stephen Dolan, and Jeremy Yallop.
+  I also want to thank to my other collaborators: Andreas Rossberg,
+  Anil Madhavapeddy, Leo White, Stephen Dolan, and Jeremy Yallop.
 
   I have had the pleasure of working in LFCS at the same time as James
   McKinna. James has always taken a genuine interest in my work and
   challenged me with intellectually stimulating questions. I
   appreciate our many conversations even though I spent days, weeks,
   sometimes months, and in some instances years to come up with
-  adequate answers. I also want to thank other former and present
-  members of Informatics: Brian Campbell, Christophe Dubach, James
-  Cheney, J. Garrett Morris, Gordon Plotkin, Michel Steuwer, Philip
-  Wadler, and Stephen Gilmore.
+  adequate answers. I also want to extend my thanks to other former
+  and present members of Informatics: Brian Campbell, Christophe
+  Dubach, James Cheney, J. Garrett Morris, Gordon Plotkin, Mary Cryan,
+  Murray Cole, Michel Steuwer, and Philip Wadler.
 
   My time as a student in Informatics Forum has been enjoyable in
   large part thanks to my friends: Amna Shahab, Chris Vasiladiotis,
@@ -348,10 +349,10 @@
   Ginsbach, Radu Ciobanu, Rajkarn Singh, Rosinda Fuentes Pineda, Rudi
   Horn, Shayan Najd, Stan Manilov, and Vanya Yaneva-Cormack.
 
-  Thanks to Ohad Kammar for agreeing to be the internal examiner for
-  my dissertation. As for external examiners, I am truly humbled and
-  thankful for Andrew Kennedy and Edwin Brady agreeing to examine my
-  dissertation.
+  Thanks to Ohad Kammar and Stephen Gilmore for agreeing to serve as
+  the internal examiners for my dissertation. As for external
+  examiners, I am truly humbled and thankful for Andrew Kennedy and
+  Edwin Brady agreeing to examine my dissertation.
 
   Throughout my studies I have received funding from the
   \href{https://www.ed.ac.uk/informatics}{School of Informatics} at
@@ -5445,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\\
@@ -5534,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
@@ -5551,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}
@@ -6546,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}
@@ -6672,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.}
@@ -12203,7 +12205,7 @@ been published previously in the following papers.
 %
 The results of Sections~\ref{sec:deep-as-shallow} and
 \ref{sec:shallow-as-deep} appear in item \ref{en:ch-def-HL18}, whilst
-the result of Section~\ref{sec:param-desugaring} appear in item
+the result of Section~\ref{sec:param-desugaring} appears in item
 \ref{en:ch-def-HLA20}.
 
 \section{Deep as shallow}
@@ -13570,10 +13572,10 @@ Figure~\ref{fig:bpcf} depicts the type syntax, type environment
 syntax, and term syntax of $\BPCF$.
 %
 The main difference in the type language between $\BCalc$ and $\BPCF$
-is that the latter does feature polymorphism and an effect tracking
-system. At the term level, $\BPCF$ does not feature polymorphic
-records and variants, but rather plain pairs and sums. For sums the
-left injection is introduced by $(\Inl~V)^B$, where the type
+is that the latter does not feature polymorphism nor an effect
+tracking system. At the term level, $\BPCF$ does not feature
+polymorphic records and variants, but rather plain pairs and sums. For
+sums the left injection is introduced by $(\Inl~V)^B$, where the type
 annotation $B$ is the type of the right injection. Similarly, the
 right injection is introduced by $(\Inl~W)^A$, where $A$ is the type
 of the left injection. The $\Case$-construct eliminates sums. The last
@@ -14258,7 +14260,8 @@ The syntax is extended as follows.
 %
 The notion of configurations changes slightly as the continuation
 component is replaced by a generalised continuation
-$\kappa \in \MGContCat$, just as described in Chapter~\ref{ch:abstract-machine}% ; a continuation is now a list of
+$\kappa \in \MGContCat$, in the same way as described in
+Chapter~\ref{ch:abstract-machine}.% ; a continuation is now a list of
 % resumptions. A resumption is a pair of a pure continuation (as in the
 % base machine) and a handler closure ($\chi$).
 %
@@ -17242,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.
@@ -17484,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.
 
@@ -17830,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
@@ -19020,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}}
@@ -19208,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}}
@@ -19733,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
@@ -19767,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
@@ -21512,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