Package the draft as an archive

Makefile

@@ -3,8 +3,10 @@ CFLAGS=-interaction=nonstopmode -halt-on-error -file-line-error
 BIBC=bibtex
 PAPER=thesis
 BIBLIO=$(PAPER)
+LATEST_COMMIT=$(shell git log --format="%h" -n 1)
 
 all: $(PAPER).pdf
+draft: $(PAPER).pdf-draft
 
 $(PAPER).aux: $(PAPER).tex
 	$(TEXC) $(CFLAGS) $(PAPER)
@@ -16,6 +18,11 @@ $(PAPER).pdf: $(PAPER).aux $(BIBLIO).bbl
 	$(TEXC) $(CFLAGS) $(PAPER)
 	$(TEXC) $(CFLAGS) $(PAPER)
 
+$(PAPER).pdf-draft: CFLAGS:=$(CFLAGS) "\def\DRAFT{$(LATEST_COMMIT)}\input{$(PAPER)}"
+$(PAPER).pdf-draft: all
+	mv $(PAPER).pdf $(PAPER)-draft.pdf
+	tar cf thesis-draft.tar.gz $(PAPER)-draft.pdf
+
 clean:
 	rm -f *.log *.aux *.toc *.out
 	rm -f *.bbl *.blg *.fls *.xml

README.md

@@ -1,6 +1,116 @@
-# PhD dissertation on foundations for programming and implementing effect handlers
+# 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.
+
+---
+
+Submitted May 30, 2021. Pending examination.
+
+The board of examiners consists of
+
+* [Andrew Kennedy](https://github.com/andrewjkennedy) (Facebook London)
+* [Edwin Brady](https://www.type-driven.org.uk/edwinb/) (University of St Andrews)
+* [Ohad Kammar](http://denotational.co.uk/) (The University of Edinburgh)
+* [Stephen Gilmore](https://homepages.inf.ed.ac.uk/stg/) (The University of Edinburgh)
+
+## Thesis structure
+
+The dissertation is structured as follows.
+
+### Introduction
+
+ * Chapter 1 puts forth an argument for why effect handlers
+   matter. Following this argument it provides a basic introduction to
+   several different approaches to effectful programming through the
+   lens of the state effect. In addition, it also declares the scope
+   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 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.
+
+### Appendices
+  * Appendix A 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
+    program and discusses it in more detail.
+
+## Building
 
 To build the dissertation you need the [Informatics thesis LaTeX
-class](https://github.com/dhil/inf-thesis-latex-cls).
+class](https://github.com/dhil/inf-thesis-latex-cls) with the
+University of Edinburgh crests. Invoking `make` on the command line
+ought to produce a PDF copy of the dissertation named `thesis.pdf`,
+e.g.
+
+```shell
+$ make
+```
 
-Don't hold your breath... This thing isn't due for a while...

thesis.tex

@@ -144,7 +144,12 @@
 % \title{Handling Computational Effects}
 % \title{Programming Computable Effectful Functions}
 % \title{Handling Effectful Computations}
-\title{Foundations for Programming and Implementing Effect Handlers}
+\ifdefined\DRAFT
+\title{Foundations for Programming and Implementing Effect Handlers\\
+       (DRAFT \href{https://github.com/dhil/phd-dissertation/commit/\DRAFT}{\DRAFT})}
+\else
+  \title{Foundations for Programming and Implementing Effect Handlers}
+\fi
 %\title{Foundations for Programming with Control via Effect Handlers}
 \author{Daniel Hillerström}