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.

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,120 @@
-# PhD dissertation on foundations for programming and implementing effect handlers
+# Foundations for programming and implementing effect handlers
+
+A copy of my dissertation can be [downloaded via my
+website](https://dhil.net/research/papers/thesis.pdf).
+
+----
+
+Submitted on May 30, 2021. Examined on August 13, 2021.
+
+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)
+* [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.
+
+### Programming
+
+ * 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 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 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.
+
+ * 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.
+
+### Expressiveness
+
+ * Chapter 6 shows that deep, shallow, and parameterised notions of
+   handlers can simulate one another up to specific notions of
+   administrative reduction.
+
+ * 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.
+
+### Conclusions
+  * Chapter 8 concludes and discusses future work.
+
+### Appendices
+
+ * 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 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.
 
-Don't hold your breath... This thing isn't due for a while...
+```shell
+$ 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.

macros.tex

@@ -4,12 +4,14 @@
 \newcommand{\defas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{=}}}
 \newcommand{\defnas}[0]{\mathrel{:=}}
 \newcommand{\simdefas}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny\text{def}}}}{\simeq}}}
+\newcommand{\adef}[0]{\mathrel{\overset{\makebox[0pt]{\mbox{\normalfont\tiny{\text{$\alpha$-def}}}}}{\simeq}}}
 
 %%
 %% Some useful maths abbreviations
 %%
 \newcommand{\C}{\ensuremath{\mathbb{C}}}
 \newcommand{\N}{\ensuremath{\mathbb{N}}}
+\newcommand{\R}{\ensuremath{\mathbb{R}}}
 \newcommand{\Z}{\ensuremath{\mathbb{Z}}}
 \newcommand{\B}{\ensuremath{\mathbb{B}}}
 \newcommand{\BB}[1]{\ensuremath{\mathbf{#1}}}
@@ -18,6 +20,11 @@
 \newcommand{\Delim}[1]{\ensuremath{\keyw{del}.#1}}
 \newcommand{\sembr}[1]{\ensuremath{\llbracket #1 \rrbracket}}
 \newcommand{\BigO}{\ensuremath{\mathcal{O}}}
+\newcommand{\SC}{\ensuremath{\mathsf{S}}}
+\newcommand{\ST}{\ensuremath{\mathsf{T}}}
+\newcommand{\ar}{\ensuremath{\mathsf{ar}}}
+\newcommand{\Tm}{\ensuremath{\mathsf{Tm}}}
+\newcommand{\Ty}{\ensuremath{\mathsf{Ty}}}
 
 %%
 %% Partiality
@@ -382,6 +389,22 @@
 % configurations
 \newcommand{\conf}{\mathcal{C}}
 
+% effect sugar
+\newcommand{\inward}[1]{\mathcal{I}\sembr{#1}}
+\newcommand{\outward}[1]{\mathcal{O}\sembr{#1}}
+\newcommand{\xcomp}[1]{\outward{#1}}
+\newcommand{\xval}[1]{\outward{#1}}
+\newcommand{\xpre}[1]{\outward{#1}}
+\newcommand{\xrow}[1]{\outward{#1}}
+\newcommand{\xeff}[1]{\outward{#1}}
+\newcommand{\pcomp}[1]{\inward{#1}}
+\newcommand{\pval}[1]{\inward{#1}}
+\newcommand{\ppre}[1]{\inward{#1}}
+\newcommand{\prow}[1]{\inward{#1}}
+\newcommand{\peff}[1]{\inward{#1}}
+\newcommand{\eamb}{\ensuremath{E_{\mathsf{amb}}}}
+\newcommand{\trval}[1]{\mathcal{T}\sembr{#1}}
+
 % UNIX example
 \newcommand{\UNIX}{UNIX}
 \newcommand{\OSname}[0]{Tiny UNIX}
@@ -507,11 +530,16 @@
 \newcommand{\Catchcont}{\keyw{catchcont}}
 \newcommand{\Control}{\keyw{control}}
 \newcommand{\Prompt}{\#}
-\newcommand{\Controlz}{\keyw{control0}}
+\newcommand{\Controlz}{\ensuremath{\keyw{control_0}}}
-\newcommand{\Promptz}{\#_0}
+\newcommand{\Spawn}{\keyw{spawn}}
+\newcommand{\Promptz}{\ensuremath{\#_0}}
 \newcommand{\Escape}{\keyw{escape}}
 \newcommand{\shift}{\keyw{shift}}
-\newcommand{\shiftz}{\keyw{shift0}}
+\newcommand{\shiftz}{\ensuremath{\keyw{shift_0}}}
+\newcommand{\CCpp}{\ensuremath{+\CC+}}
+\newcommand{\CCpm}{\ensuremath{+\CC-}}
+\newcommand{\CCmp}{\ensuremath{-\CC+}}
+\newcommand{\CCmm}{\ensuremath{-\CC-}}
 \def\sigh#1{%
 \pmb{\left\langle\vphantom{#1}\right.}%
 #1%
@@ -519,6 +547,8 @@
 \newcommand{\llambda}{\ensuremath{\pmb{\lambda}}}
 \newcommand{\reset}[1]{\pmb{\langle} #1 \pmb{\rangle}}
 \newcommand{\resetz}[1]{\pmb{\langle} #1 \pmb{\rangle}_0}
+\newcommand{\dollarz}[2]{\ensuremath{\reset{#2 \mid #1}}}
+\newcommand{\dollarzh}[2]{\ensuremath{#1\,\$_0#2}}
 \newcommand{\fcontrol}{\keyw{fcontrol}}
 \newcommand{\fprompt}{\%}
 \newcommand{\splitter}{\keyw{splitter}}
@@ -546,6 +576,7 @@
 %%
 %% Asymptotic improvement macros
 %%
+\newcommand{\LLL}{\ensuremath{\mathcal L}}
 \newcommand{\naive}{naïve\xspace}
 \newcommand{\naively}{naïvely\xspace}
 \newcommand{\Naive}{Naïve\xspace}
@@ -680,3 +711,141 @@
     }
 ;
 \end{tikzpicture}}
+
+\newcommand{\smath}[1]{\ensuremath{{\scriptstyle #1}}}
+
+\newcommand{\InfiniteModel}{%
+\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 3.0cm/##1,
+    level distance = 1.0cm}]
+\node (root) [draw=none] { }
+  child { node [opnode] {$\smath{\query 0}$}
+    child { node [opnode] {$\smath{\query 0}$}
+      child { node [draw=none,rotate=165] {$\vdots$}
+        edge from parent node { }
+      }
+      child { node[leaf] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    child { node [leaf] {$\smath{\ans\False}$}
+      edge from parent node { }
+    }
+    edge from parent node { }
+  }
+;
+\end{tikzpicture}}
+%
+\newcommand{\ShortConjModel}{%
+\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 3.5cm/##1,
+    level distance = 1.0cm}]
+\node (root) [draw=none] { }
+  child { node [opnode] {$\smath{\query 0}$}
+    child { node [opnode] {$\smath{\query 0}$}
+      child { node [treenode] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      child { node[treenode] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    child { node [treenode] {$\smath{\ans\False}$}
+      edge from parent node { }
+    }
+    edge from parent node { }
+  }
+;
+\end{tikzpicture}}
+%
+
+\newcommand{\TTTwoModel}{%
+\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 8cm/##1,
+    level distance = 1.5cm}]
+\node (root) [draw=none] { }
+  child { node [opnode] {$\smath{\query 0}$}
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [leaf] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      child { node[leaf] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [leaf] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      child { node[leaf] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    edge from parent node { }
+  }
+;
+\end{tikzpicture}}
+%
+\newcommand{\XORTwoModel}{%
+\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 5.5cm/##1,
+    level distance = 1cm}]
+\node (root) [draw=none] { }
+  child { node [opnode] {$\smath{\query 0}$}
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [treenode] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      child { node[treenode] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [treenode] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      child { node[treenode] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    edge from parent node { }
+  }
+;
+\end{tikzpicture}}
+%
+\newcommand{\SXORTwoModel}{%
+\begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 2.5cm/##1,
+    level distance = 1cm}]
+\node (root) [opnode] {$\smath{\query 0}$}
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [treenode] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      child { node[treenode] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+    child { node [opnode] {$\smath{\query 1}$}
+      child { node [treenode] {$\smath{\ans\True}$}
+        edge from parent node { }
+      }
+      child { node[treenode] {$\smath{\ans\False}$}
+        edge from parent node { }
+      }
+      edge from parent node { }
+    }
+;
+\end{tikzpicture}}
+%
+\newcommand{\TTZeroModel}{%
+  \begin{tikzpicture}[->,>=stealth',level/.style={sibling distance = 1cm/##1,
+    level distance = 1cm}]
+  \node (root) [draw=none] { }
+  child { node [treenode] {$\smath{\ans\True}$}
+    edge from parent node { }
+  }
+;
+\end{tikzpicture}}%

slides/Makefile

@@ -0,0 +1,32 @@
+TEXC=pdflatex
+CFLAGS=-interaction=nonstopmode -halt-on-error -file-line-error
+BIBC=bibtex
+PAPER=viva
+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)
+
+$(BIBLIO).bbl: $(PAPER).aux $(BIBLIO).bib
+	$(BIBC) $(PAPER)
+
+$(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
+	rm -f *.nav *.snm
+	rm -f *.fdb_latexmk *.vtc *.cut
+	rm -f $(PAPER).pdf camera-ready.pdf submission.pdf
+	rm -f *.o *.cmx *.cmo

slides/viva.bib

@@ -0,0 +1,82 @@
+@inproceedings{HillerstromL16,
+  author    = {Daniel Hillerstr{\"{o}}m and
+               Sam Lindley},
+  title     = {Liberating effects with rows and handlers},
+  booktitle = {TyDe@ICFP},
+  pages     = {15--27},
+  publisher = {{ACM}},
+  year      = {2016}
+}
+
+@inproceedings{HillerstromLAS17,
+  author    = {Daniel Hillerstr{\"{o}}m and
+               Sam Lindley and
+               Robert Atkey and
+               {KC} Sivaramakrishnan},
+  title     = {Continuation Passing Style for Effect Handlers},
+  booktitle = {{FSCD}},
+  series    = {LIPIcs},
+  volume    = {84},
+  pages     = {18:1--18:19},
+  OPTpublisher = {Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik},
+  year      = {2017}
+}
+
+@inproceedings{HillerstromL18,
+  author    = {Daniel Hillerstr{\"{o}}m and
+               Sam Lindley},
+  title     = {Shallow Effect Handlers},
+  booktitle = {{APLAS}},
+  OPTseries    = {Lecture Notes in Computer Science},
+  series    = {{LNCS}},
+  volume    = {11275},
+  pages     = {415--435},
+  publisher = {Springer},
+  year      = {2018}
+}
+
+@article{HillerstromLA20,
+  author    = {Daniel Hillerstr{\"{o}}m and
+               Sam Lindley and
+               Robert Atkey},
+  title     = {Effect handlers via generalised continuations},
+  journal   = {J. Funct. Program.},
+  volume    = {30},
+  pages     = {e5},
+  year      = {2020}
+}
+
+@article{HillerstromLL20,
+  author    = {Daniel Hillerstr{\"{o}}m and
+               Sam Lindley and
+               John Longley},
+  title     = {Effects for Efficiency: Asymptotic Speedup with First-Class Control},
+  journal   = {Proc. {ACM} Program. Lang.},
+  volume    = {4},
+  number    = {{ICFP}},
+  pages     = {100:1--100:29},
+  year      = {2020}
+}
+
+# Unix
+@article{RitchieT74,
+  author    = {Dennis Ritchie and
+               Ken Thompson},
+  title     = {The {UNIX} Time-Sharing System},
+  journal   = {Commun. {ACM}},
+  volume    = {17},
+  number    = {7},
+  pages     = {365--375},
+  year      = {1974}
+}
+
+# CEK & C
+@InProceedings{FelleisenF86,
+  title={Control Operators, the {SECD}-machine, and the $\lambda$-Calculus},
+  author={Felleisen, Matthias and Friedman, Daniel P.},
+  year=1987,
+  booktitle = {Formal Description of Programming Concepts III},
+  OPTbooktitle = {The Proceedings of the Conference on Formal Description of Programming Concepts III, Ebberup, Denmark},
+  pages     = {193--217},
+  OPTpublisher={North Holland}
+}

slides/viva.tex

@@ -0,0 +1,201 @@
+\documentclass[169,10pt,compress,dvipsnames]{beamer}
+%%
+%% Slides layout
+%%
+\beamertemplatenavigationsymbolsempty  % hides navigation buttons
+\usetheme{Madrid}                      % standard Madrid theme
+\setbeamertemplate{footline}{}         % renders the footer empty
+%
+\setbeamertemplate{bibliography item}{ % this is a hack to prevent Madrid theme + biblatex
+  \hspace{-0.4cm}\lower3pt\hbox{       % from causing bibliography entries to run over
+    \pgfuseimage{beamericonarticle}    % the slide margins
+}}
+
+%%
+%% Packages
+%%
+\usepackage[utf8]{inputenc}               % enable UTF-8 compatible typing
+\usepackage{hyperref}                     % interactive PDF
+\usepackage[sort&compress,square,numbers]{natbib}    % Bibliography
+\usepackage{bibentry}         % Print bibliography entries inline.
+\makeatletter                 % Redefine bibentry to omit hyperrefs
+\renewcommand\bibentry[1]{\nocite{#1}{\frenchspacing
+     \@nameuse{BR@r@#1\@extra@b@citeb}}}
+\makeatother
+\nobibliography*              % use the bibliographic data from the standard BibTeX setup.
+\usepackage{amsmath,amssymb,mathtools}    % maths typesetting
+\usepackage{../pkgs/mathpartir}           % Inference rules
+\usepackage{../pkgs/mathwidth}            % renders character sequences nicely in math mode
+\usepackage{stmaryrd}                     % semantic brackets
+\usepackage{xspace}                       % proper spacing for macros in text
+
+\usepackage[T1]{fontenc}                  % 8-bit font encoding
+                                          % native support for accented characters.
+\usepackage[scaled=0.85]{beramono}        % smoother typewriter font
+\newcommand*{\Scale}[2][4]{\scalebox{#1}{\ensuremath{#2}}}%
+
+\input{../macros.tex}
+
+%%
+%% Meta information
+%%
+\author{Daniel Hillerström}
+\title{Foundations for Programming and Implementing Effect Handlers}
+\institute{The University of Edinburgh, Scotland UK}
+\subtitle{PhD viva}
+\date{August 13, 2021}
+
+%%
+%% Slides
+%%
+\begin{document}
+
+%
+% Title slide
+%
+\begin{frame}
+  \maketitle
+\end{frame}
+
+% Dissertation overview
+\begin{frame}
+  \frametitle{My dissertation at glance}
+
+  Three main strands of work
+
+  \begin{description}
+  \item[Programming] Language design and applications of effect handlers.
+  \item[Implementation] Canonical implementation strategies for effect handlers.
+  \item[Expressiveness] Exploration of the computational expressiveness of effect handlers.
+  \end{description}
+\end{frame}
+
+\begin{frame}
+  \frametitle{Calculi for deep, shallow, and parameterised handlers}
+
+  The calculi capture key aspects of the implementation of effect
+  handlers in Links.
+
+  \begin{itemize}
+    \item $\HCalc$ ordinary deep handlers (fold).
+    \item $\SCalc$ shallow handlers (case-split).
+    \item $\HPCalc$ parameterised deep handlers (fold+state).
+  \end{itemize}
+
+  The actual implementation is the union of the three calculi.\\[2em]
+
+  \textbf{Relevant papers} TyDe'16~\cite{HillerstromL16},
+  APLAS'18~\cite{HillerstromL18}, JFP'20~\cite{HillerstromLA20}.
+\end{frame}
+
+% UNIX
+\begin{frame}
+  \frametitle{Effect handlers as composable operating systems}
+
+  An interpretation of \citeauthor{RitchieT74}'s
+  UNIX~\cite{RitchieT74} in terms of effect handlers.\\[2em]
+
+  \[
+    \bl
+    \!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\!\textbf{Basic idea}
+      \ba[m]{@{\qquad}r@{~}c@{~}l}
+        \text{\emph{system call}} &\approx& \text{\emph{operation invocation}}\\
+        \text{\emph{system call implementation}} &\approx& \text{\emph{operation interpretation}}
+      \ea
+    \el
+  \]\hfill\\[2em]
+
+  \textbf{Key point} Legacy code is modularly retrofitted with functionality.
+\end{frame}
+
+% CPS translation
+\begin{frame}
+  \frametitle{CPS transforms for effect handlers}
+
+  A higher-order CPS transform for effect handlers with generalised
+  continuations.\\[1em]
+
+  \textbf{Generalised continuation} Structured representation of
+  delimited continuations.\\[0.5em]
+
+  \[
+    \Scale[1.8]{\kappa = \overline{(\sigma, (\hret,\hops))}}
+  \]\\[1em]
+
+  \textbf{Key point} Separate the \emph{doing} layer ($\sigma$) from the \emph{being} layer ($H$).\\[2em]
+
+  \textbf{Relevant papers} FSCD'17~\cite{HillerstromLAS17},
+  APLAS'18~\cite{HillerstromL18}, JFP'20~\cite{HillerstromLA20}.
+\end{frame}
+
+% Abstract machine
+\begin{frame}
+  \frametitle{Abstract machine semantics for effect handlers}
+
+  Plugging generalised continuations into \citeauthor{FelleisenF86}'s
+  CEK machine~\cite{FelleisenF86} yields a runtime for effect
+  handlers.\\[2em]
+
+  \[
+    \Scale[2]{\cek{C \mid E \mid K = \overline{(\sigma, (H,E))}}}
+  \]\\[2em]
+
+  \textbf{Relevant papers} TyDe'16~\cite{HillerstromL16},
+  JFP'20~\cite{HillerstromLA20}.
+
+\end{frame}
+
+% Interdefinability of handlers
+\begin{frame}
+  \frametitle{Interdefinability of effect handlers}
+
+  Deep, shallow, and parameterised handlers are interdefinable
+  w.r.t. to typability-preserving macro-expressiveness.
+
+  \begin{itemize}
+    \item Deep as shallow, $\mathcal{D}\llbracket - \rrbracket$, image is computationally lightweight.
+    \item Shallow as deep, $\mathcal{S}\llbracket - \rrbracket$, image is computationally expensive.
+    \item Parameterised as deep, $\mathcal{P}\llbracket - \rrbracket$,
+      image uses explicit state-passing.
+    \end{itemize}
+    ~\\[1em]
+    \textbf{Relevant papers} APLAS'18~\cite{HillerstromL18},
+    JFP'20~\cite{HillerstromLA20}.
+
+\end{frame}
+
+% Asymptotic speed up with first-class control
+\begin{frame}
+  \frametitle{Asymptotic speed up with effect handlers}
+
+  Effect handlers can make some programs faster!
+
+  \[
+    \Count_n : ((\Nat_n \to \Bool) \to \Bool) \to \Nat
+  \]\\[1em]
+  %
+  Using type-respecting expressiveness
+  \begin{itemize}
+  \item There \textbf{exists} an implementation of $\Count_n \in \HPCF$ with
+    effect handlers such that the runtime for every $n$-standard predicate $P$ is
+    $\Count_n~P = \BigO(2^n)$.
+  \item \textbf{Forall} implementations of $\Count_n \in \BPCF$ the runtime for every $n$-standard predicate $P$ is $\Count_n~P = \Omega(n2^n)$
+  \end{itemize}
+  ~\\[1em]
+  \textbf{Relevant paper} ICFP'20~\cite{HillerstromLL20}.
+\end{frame}
+
+% Background
+% \begin{frame}
+%   \frametitle{Continuations literature review}
+% \end{frame}
+
+%
+% References
+%
+\begin{frame}%[allowframebreaks]
+  \frametitle{References}
+  \bibliographystyle{plainnat}
+  \bibliography{\jobname}
+\end{frame}
+\end{document}

thesis.bib

@@ -1,4 +1,4 @@
-# Daniel's master's thesis (initial implementation of handlers in Links)
+# My MSc thesis (initial implementation of handlers in Links)
 @MastersThesis{Hillerstrom15,
   author    = {Daniel Hillerström},
   title     = {Handlers for Algebraic Effects in {Links}},
@@ -8,7 +8,7 @@
   year      = 2015
 }
 
-# Daniel's master's thesis (abstract message-passing concurrency model, compilation of handlers)
+# My MSc(R) thesis (abstract message-passing concurrency model, compilation of handlers)
 @MastersThesis{Hillerstrom16,
   author    = {Daniel Hillerström},
   title     = {Compilation of Effect Handlers and their Applications in Concurrency},
@@ -19,6 +19,15 @@
   type      = {{MSc(R)} thesis}
 }
 
+# UNIX with effect handlers abstract
+@misc{Hillerstrom21,
+  author = {Daniel Hillerström},
+  title  = {Composing {UNIX} with {Effect} {Handlers}: {A} {Case} {Study} in {Effect} {Handler} {Oriented} {Programming} (Extended Abstract)},
+  year   = {2021},
+  optmonth  = sep,
+  howpublished = {{ML Workshop}}
+}
+
 # OCaml handlers
 @article{SivaramakrishnanDWKJM21,
   author    = {{KC} Sivaramakrishnan and
@@ -27,7 +36,7 @@
                Tom Kelly and
                Sadiq Jaffer and
                Anil Madhavapeddy},
-  title     = {Retrofitting Effect Handlers onto OCaml},
+  title     = {Retrofitting Effect Handlers onto {OCaml}},
   journal   = {CoRR},
   volume    = {abs/2104.00250},
   year      = {2021}
@@ -35,16 +44,17 @@
 
 @misc{DolanWSYM15,
   title     = {Effective Concurrency through Algebraic Effects},
-  author = {Stephen Dolan and Leo White and {KC} Sivaramakrishnan and Jeremy Yallop and Anil Madhavapeddy},
+  author    = {Stephen Dolan and Leo White and {KC} Sivaramakrishnan
+               and Jeremy Yallop and Anil Madhavapeddy},
   year      = 2015,
-  howpublished = {OCaml Workshop}
+  howpublished = {{OCaml} Workshop}
 }
 
 @misc{DolanWM14,
   title     = {Multicore {OCaml}},
   author    = {Stephen Dolan and Leo White and Anil Madhavapeddy},
   year      = {2014},
-  howpublished = {OCaml Workshop}
+  howpublished = {{OCaml} Workshop}
 }
 
 @inproceedings{DolanEHMSW17,
@@ -67,7 +77,7 @@
 # Delimited control in OCaml
 @article{Kiselyov12,
   author    = {Oleg Kiselyov},
-  title     = {Delimited control in OCaml, abstractly and concretely},
+  title     = {Delimited control in {OCaml}, abstractly and concretely},
   journal   = {Theor. Comput. Sci.},
   volume    = {435},
   pages     = {56--76},
@@ -278,6 +288,16 @@
   year      = {2020}
 }
 
+@article{HillerstromLL20a,
+  author    = {Daniel Hillerstr{\"{o}}m and
+               Sam Lindley and
+               John Longley},
+  title     = {Effects for Efficiency: Asymptotic Speedup with First-Class Control},
+  journal   = {CoRR},
+  volume    = {abs/2007.00605},
+  year      = {2020}
+}
+
 @phdthesis{McLaughlin20,
   author    = {Craig McLaughlin},
   title     = {Relational Reasoning for Effects and Handlers},
@@ -357,7 +377,7 @@
 @inproceedings{XieL20,
   author    = {Ningning Xie and
                Daan Leijen},
-  title     = {Effect handlers in Haskell, evidently},
+  title     = {Effect handlers in {Haskell}, evidently},
   booktitle = {Haskell@ICFP},
   pages     = {95--108},
   publisher = {{ACM}},
@@ -581,16 +601,6 @@
   year      = {2017}
 }
 
-@inproceedings{Leijen05,
-  author    = {Daan Leijen},
-  title     = {Extensible records with scoped labels},
-  booktitle = {Trends in Functional Programming},
-  series    = {Trends in Functional Programming},
-  volume    = {6},
-  pages     = {179--194},
-  publisher = {Intellect},
-  year      = {2005}
-}
 
 # Helium
 @article{BiernackiPPS18,
@@ -741,6 +751,19 @@
   year      = {2012}
 }
 
+# "Proto handlers"
+@inproceedings{CartwrightF94,
+  author    = {Robert Cartwright and
+               Matthias Felleisen},
+  title     = {Extensible Denotational Language Specifications},
+  booktitle = {{TACS}},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {789},
+  pages     = {244--272},
+  publisher = {Springer},
+  year      = {1994}
+}
+
 # Applicative idioms
 @article{McBrideP08,
   author    = {Conor McBride and
@@ -835,6 +858,16 @@
   year      = {1995}
 }
 
+@article{Sabry98,
+  author    = {Amr Sabry},
+  title     = {What is a Purely Functional Language?},
+  journal   = {J. Funct. Program.},
+  volume    = {8},
+  number    = {1},
+  pages     = {1--22},
+  year      = {1998}
+}
+
 @article{Swierstra08,
   author    = {Wouter Swierstra},
   title     = {Data types {\`{a}} la carte},
@@ -1171,6 +1204,50 @@
   year      = {2006}
 }
 
+# Row polymorphism
+@inproceedings{Wand87,
+  author    = {Mitchell Wand},
+  title     = {Complete Type Inference for Simple Objects},
+  booktitle = {{LICS}},
+  pages     = {37--44},
+  publisher = {{IEEE} Computer Society},
+  year      = {1987}
+}
+
+@inbook{Remy94,
+  author    = {Didier R\'{e}my},
+  title     = {Type Inference for Records in Natural Extension of ML},
+  year      = 1994,
+  OPTisbn = {026207155X},
+  publisher = {MIT Press},
+  address = {Cambridge, MA, USA},
+  booktitle = {Theoretical Aspects of Object-Oriented Programming: Types, Semantics, and Language Design},
+  pages     = {67--95},
+  numpages  = {29}
+}
+
+@inproceedings{Leijen05,
+  author    = {Daan Leijen},
+  title     = {Extensible records with scoped labels},
+  booktitle = {Trends in Functional Programming},
+  series    = {Trends in Functional Programming},
+  volume    = {6},
+  pages     = {179--194},
+  publisher = {Intellect},
+  year      = {2005}
+}
+
+@article{MorrisM19,
+  author    = {J. Garrett Morris and
+               James McKinna},
+  title     = {Abstracting extensible data types: or, rows by any other name},
+  journal   = {Proc. {ACM} Program. Lang.},
+  volume    = {3},
+  number    = {{POPL}},
+  pages     = {12:1--12:28},
+  year      = {2019}
+}
+
 # fancy row typing systems that support shapes
 @inproceedings{BerthomieuS95,
   author = {Bernard Berthomieu and Camille le Moniès de Sagazan},
@@ -1181,13 +1258,12 @@
 
 @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},
 }
 
-
 # Zipper data structure.
 @article{Huet97,
   author    = {G{\'{e}}rard P. Huet},
@@ -1203,9 +1279,6 @@
   OPTbibsource = {dblp computer science bibliography, http://dblp.org}
 }
 
-
-
-
 @article{Hughes00,
   author    = {John Hughes},
   title     = {Generalising monads to arrows},
@@ -1738,6 +1811,18 @@
   year      = {1990}
 }
 
+@inproceedings{KameyamaY08,
+  author    = {Yukiyoshi Kameyama and
+               Takuo Yonezawa},
+  title     = {Typed Dynamic Control Operators for Delimited Continuations},
+  booktitle = {{FLOPS}},
+  series    = {{LNCS}},
+  volume    = {4989},
+  pages     = {239--254},
+  publisher = {Springer},
+  year      = {2008}
+}
+
 # Escape
 @article{Reynolds98a,
   author    = {John C. Reynolds},
@@ -1929,6 +2014,20 @@
   year      = {1994}
 }
 
+# marker and callpc
+@inproceedings{MoreauQ94,
+  author    = {Luc Moreau and
+               Christian Queinnec},
+  title     = {Partial Continuations as the Difference of Continuations - {A} Duumvirate
+               of Control Operators},
+  booktitle = {{PLILP}},
+  series    = {{LNCS}},
+  volume    = {844},
+  pages     = {182--197},
+  publisher = {Springer},
+  year      = {1994}
+}
+
 # Comparison of (some) delimited control operators
 @misc{Shan04,
   author    = {Chung{-}chieh Shan},
@@ -2302,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,
@@ -3443,6 +3543,18 @@
   year      = {1992}
 }
 
+@inproceedings{TofteT94,
+  author    = {Mads Tofte and
+               Jean{-}Pierre Talpin},
+  title     = {Implementation of the Typed Call-by-Value lambda-Calculus using a
+               Stack of Regions},
+  booktitle = {{POPL}},
+  pages     = {188--201},
+  publisher = {{ACM} Press},
+  year      = {1994}
+}
+
+
 @article{TofteT97,
   author    = {Mads Tofte and
                Jean{-}Pierre Talpin},
@@ -3466,6 +3578,26 @@
   year      = {1999}
 }
 
+@inproceedings{BentonB07,
+  author    = {Nick Benton and
+               Peter Buchlovsky},
+  title     = {Semantics of an effect analysis for exceptions},
+  booktitle = {{TLDI}},
+  pages     = {15--26},
+  publisher = {{ACM}},
+  year      = {2007}
+}
+
+@article{BentonK99,
+  author    = {Nick Benton and
+               Andrew Kennedy},
+  title     = {Monads, Effects and Transformations},
+  journal   = {Electron. Notes Theor. Comput. Sci.},
+  volume    = {26},
+  pages     = {3--20},
+  year      = {1999}
+}
+
 # Intensional type theory
 @book{MartinLof84,
   author    = {Per Martin{-}L{\"{o}}f},
@@ -3511,3 +3643,161 @@
   school    = {The University of Edinburgh, {UK}},
   year      = {2010}
 }
+
+# Functional programming
+@article{Hughes89,
+  author    = {John Hughes},
+  title     = {Why Functional Programming Matters},
+  journal   = {Comput. J.},
+  volume    = {32},
+  number    = {2},
+  pages     = {98--107},
+  year      = {1989}
+}
+
+# Curry-Howard correspondence
+@incollection{Howard80,
+  author    = {William A. Howard},
+  title     = {The Formulae-as-Types Notion of Construction},
+  booktitle = {To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus, and Formalism},
+  publisher = {Academic Press},
+  editor    = {Haskell Curry and Hindley B. and Seldin J. Roger and P. Jonathan},
+  year      = 1980
+}
+
+# Criteria for modular programming
+@article{Parnas72,
+  author    = {David Lorge Parnas},
+  title     = {On the Criteria To Be Used in Decomposing Systems into Modules},
+  journal   = {Commun. {ACM}},
+  volume    = {15},
+  number    = {12},
+  pages     = {1053--1058},
+  year      = {1972}
+}
+
+# The universal type
+@InProceedings{Longley03,
+  author    = {John Longley},
+  title     = {Universal Types and What They are Good For},
+  booktitle = {Domain Theory, Logic and Computation},
+  year      = 2003,
+  publisher = {Springer Netherlands},
+  pages     = {25--63},
+  OPTisbn   = {978-94-017-1291-0}
+}
+
+# Sixth order function example
+@article{Okasaki98,
+  author    = {Chris Okasaki},
+  title     = {Functional Pearl: Even Higher-Order Functions for Parsing},
+  journal   = {J. Funct. Program.},
+  volume    = {8},
+  number    = {2},
+  pages     = {195--199},
+  year      = {1998}
+}
+
+# CLR
+@book{CormenLRS09,
+  author = {Cormen, Thomas H. and Leiserson, Charles E. and Rivest, Ronald L. and Stein, Clifford},
+  title = {Introduction to Algorithms, Third Edition},
+  year = {2009},
+  publisher = {{MIT} Press},
+  edition = {3rd},
+}
+
+# Undelimited continuations survey
+@unpublished{FelleisenS99,
+  author = {Matthias Felleisen and Amr Sabry},
+  title  = {Continuations in Programming Practice: Introduction and Survey},
+  year   = 1999,
+  month  = aug,
+  note   = {Draft}
+}
+
+# TypeScript
+@inproceedings{BiermanAT14,
+  author    = {Gavin M. Bierman and
+               Mart{\'{\i}}n Abadi and
+               Mads Torgersen},
+  title     = {Understanding TypeScript},
+  booktitle = {{ECOOP}},
+  series    = {{LNCS}},
+  volume    = {8586},
+  pages     = {257--281},
+  publisher = {Springer},
+  year      = {2014}
+}
+
+# TT lifting
+@inproceedings{LindleyS05,
+  author    = {Sam Lindley and
+               Ian Stark},
+  title     = {Reducibility and TT-Lifting for Computation Types},
+  booktitle = {{TLCA}},
+  series    = {Lecture Notes in Computer Science},
+  volume    = {3461},
+  pages     = {262--277},
+  publisher = {Springer},
+  year      = {2005}
+}
+
+# Three state equations
+@inproceedings{Mellies14,
+  author    = {Paul{-}Andr{\'{e}} Melli{\`{e}}s},
+  title     = {Local States in String Diagrams},
+  booktitle = {{RTA-TLCA}},
+  series    = {{LNCS}},
+  volume    = {8560},
+  pages     = {334--348},
+  publisher = {Springer},
+  year      = {2014}
+}
+
+# Asymptotic notation
+@book{Bachmann94,
+  author    = {Paul Bachmann},
+  title     = {Die Analytische Zahlentheorie},
+  publisher = {Teubner},
+  pages     = {1--494},
+  year      = 1894
+}
+
+# Game semantics
+@inbook{Hyland97,
+   author   = {Martin Hyland},
+   title    = {Game Semantics},
+   booktitle = {Semantics and Logics of Computation},
+   publisher = {Cambridge University Press},
+   editor   = {Andrew M. Pitts and Peter Dybjer},
+   pages    = {131--184},
+   year     = 1997
+}
+
+# Milner's context lemma
+@article{Milner77,
+  author    = {Robin Milner},
+  title     = {Fully Abstract Models of Typed $\lambda$-Calculi},
+  journal   = {Theor. Comput. Sci.},
+  volume    = {4},
+  number    = {1},
+  pages     = {1--22},
+  year      = {1977}
+}
+
+# Dagstuhl seminar report
+@article{AhmanALR21,
+  author    = {Danel Ahman and
+               Amal Ahmed and
+               Sam Lindley and
+               Andreas Rossberg},
+  title     = {{Scalable} {Handling} of {Effects} ({Dagstuhl} {Seminar} 21292)},
+  journal   = {Dagstuhl Reports},
+  volume    = {11},
+  number    = {6},
+  pages     = {54--81},
+  year      = {2021}
+}
+
+