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
+A copy of my dissertation can be [downloaded via my
-this repository. I ask that you **do not** link to or distribute the
+website](https://dhil.net/research/papers/thesis.pdf).
-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.
 
----
+----
 
-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,77 +27,76 @@ 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
+ * Chapter 2 illustrates effect handler oriented programming by
-calculus, λ<sub>b</sub>, which makes key use of Remy-style row polymorphism
+   example by implementing a small operating system dubbed Tiny UNIX,
-to implement polymorphic variants, structural records, and a
+   which captures some essential traits of Ritchie and Thompson's
-structural effect system. The calculus distils the essence of the core
+   UNIX. The implementation starts with a basic notion of file i/o,
-of the Links programming language.
+   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>,
+ * Chapter 3 introduces a polymorphic fine-grain call-by-value core
-which are λ<sub>h</sub> that adds deep handlers, λ<sup>†</sup> that adds shallow
+   calculus, λ<sub>b</sub>, which makes key use of Rémy-style row
-handlers, and λ<sup>‡</sup> that adds parameterised handlers. The chapter
+   polymorphism to implement polymorphic variants, structural records,
-also contains a running case study that demonstrates effect handler
+   and a structural effect system. The calculus distils the essence of
-oriented programming in practice by implementing a small operating
+   the core of the Links programming language. The chapter also
-system dubbed Tiny UNIX based on Ritchie and Thompson's original
+   presents three extensions of λ<sub>b</sub>, which are λ<sub>h</sub>
-UNIX.
+   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
+ * Chapter 4 develops a higher-order continuation passing style
-style translation for effect handlers through a series of step-wise
+   translation for effect handlers through a series of step-wise
-refinements of an initial standard continuation passing style
+   refinements of an initial standard continuation passing style
-translation for λ<sub>b</sub>. Each refinement slightly modifies the notion
+   translation for λ<sub>b</sub>. Each refinement slightly modifies
-of continuation employed by the translation. The development
+   the notion of continuation employed by the translation. The
-ultimately leads to the key invention of generalised continuation,
+   development ultimately leads to the key invention of generalised
-which is used to give a continuation passing style semantics to deep,
+   continuation, which is used to give a continuation passing style
-shallow, and parameterised handlers.
+   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
+   to abstract machine as we plug generalised continuations into
-Felleisen and Friedman's CEK machine to obtain an adequate abstract
+   Felleisen and Friedman's CEK machine to obtain an adequate abstract
-runtime with simultaneous support for deep, shallow, and parameterised
+   runtime with simultaneous support for deep, shallow, and
-handlers.
+   parameterised handlers.
 
 ### Expressiveness
- * Chapter 8 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 6 shows that deep, shallow, and parameterised notions of
-this chapter, we show that effect handlers enable an asymptotic
+   handlers can simulate one another up to specific notions of
-improvement in runtime complexity for a certain class of
+   administrative reduction.
-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
+ * Chapter 7 studies the fundamental efficiency of effect handlers. In
-λ<sub>b</sub>) and its extension with effect handlers λ<sub>h</sub><sup>→</sup>.  We
+   this chapter, we show that effect handlers enable an asymptotic
-show that λ<sub>h</sub><sup>→</sup> admits an asymptotically more efficient
+   improvement in runtime complexity for a certain class of
-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
+
-    state is redundant.
+ * Appendix A contains a literature survey of continuations and
-  * Appendix B contains the proof details for the higher-order
+   first-class control. I classify continuations according to their
-    uncurried CPS translation for deep and shallow handlers.
+   operational behaviour and provide an overview of the various
-  * Appendix C contains the proof details and gadgetry for the
+   first-class sequential control operators that appear in the
-    complexity of the effectful generic count program.
+   literature. The application spectrum of continuations is discussed
-  * Appendix D provides a sample implementation of the Berger count
+   as well as implementation strategies for first-class control.
-    program and discusses it in more detail.
+ * Appendix B contains a proof that shows the `Get-get` equation for
+   state is redundant.
+ * 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
+   program and discusses it in more detail.
 
 ## Building
 
@@ -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,