Dissertation overview

README.md

@@ -16,6 +16,72 @@ The board of examiners consists of
 * Ohad Kammar (The University of Edinburgh)
 * Stephen Gilmore (The University of Edinburgh)
 
+## Thesis structure
+
+The dissertation is structured as follows.
+
+### 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 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.
+
+### Implementation
+
+ * Chapter 6 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.
+
+ * Chapter 7 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.
+
+### 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
+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.
+
+### Conclusions
+  * Chapter 10 concludes and discusses future work.
+
 ## Building
 
 To build the dissertation you need the [Informatics thesis LaTeX