|
|
|
|
%% 12pt font size, PhD thesis, LFCS, print twosided, new chapters on right page
|
|
|
|
|
\documentclass[12pt,phd,lfcs,twoside,openright,logo,leftchapter,normalheadings]{infthesis}
|
|
|
|
|
\shieldtype{0}
|
|
|
|
|
|
|
|
|
|
%% Packages
|
|
|
|
|
\usepackage[utf8]{inputenc} % Enable UTF-8 typing
|
|
|
|
|
\usepackage[british]{babel} % British English
|
|
|
|
|
\usepackage[breaklinks]{hyperref} % Interactive PDF
|
|
|
|
|
\usepackage{url}
|
|
|
|
|
\usepackage{breakurl}
|
|
|
|
|
\usepackage{amsmath} % Mathematics library
|
|
|
|
|
\usepackage{amssymb} % Provides math fonts
|
|
|
|
|
\usepackage{amsthm} % Provides \newtheorem, \theoremstyle, etc.
|
|
|
|
|
\usepackage{mathtools}
|
|
|
|
|
\usepackage{pkgs/mathpartir} % Inference rules
|
|
|
|
|
\usepackage{stmaryrd} % semantic brackets
|
|
|
|
|
\usepackage{array}
|
|
|
|
|
\usepackage{float} % Float control
|
|
|
|
|
\usepackage{caption,subcaption} % Sub figures support
|
|
|
|
|
\usepackage[T1]{fontenc} % Fixes font issues
|
|
|
|
|
\usepackage{lmodern}
|
|
|
|
|
\usepackage{enumerate} % Customise enumerate-environments
|
|
|
|
|
\usepackage{xcolor} % Colours
|
|
|
|
|
\usepackage{tikz}
|
|
|
|
|
\usetikzlibrary{fit,calc,trees,positioning,arrows,chains,shapes.geometric,%
|
|
|
|
|
decorations.pathreplacing,decorations.pathmorphing,shapes,%
|
|
|
|
|
matrix,shapes.symbols,intersections}
|
|
|
|
|
|
|
|
|
|
%% Information about the title, etc.
|
|
|
|
|
% \title{Higher-Order Theories of Handlers for Algebraic Effects}
|
|
|
|
|
\title{Handlers for Algebraic Effects: Applications, Compilation, and Expressiveness}
|
|
|
|
|
\author{Daniel Hillerström}
|
|
|
|
|
|
|
|
|
|
%% If the year of submission is not the current year, uncomment this line and
|
|
|
|
|
%% specify it here:
|
|
|
|
|
\submityear{2020}
|
|
|
|
|
|
|
|
|
|
%% Specify the abstract here.
|
|
|
|
|
\abstract{%
|
|
|
|
|
An abstract\dots
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
%% Now we start with the actual document.
|
|
|
|
|
\begin{document}
|
|
|
|
|
\raggedbottom
|
|
|
|
|
%% First, the preliminary pages
|
|
|
|
|
\begin{preliminary}
|
|
|
|
|
|
|
|
|
|
%% This creates the title page
|
|
|
|
|
\maketitle
|
|
|
|
|
|
|
|
|
|
%% Acknowledgements
|
|
|
|
|
\begin{acknowledgements}
|
|
|
|
|
List of people to thank
|
|
|
|
|
\begin{itemize}
|
|
|
|
|
\item Sam Lindley
|
|
|
|
|
\item John Longley
|
|
|
|
|
\item Christophe Dubach
|
|
|
|
|
\item KC Sivaramakrishnan
|
|
|
|
|
\item Stephen Dolan
|
|
|
|
|
\item Anil Madhavapeddy
|
|
|
|
|
\item Gemma Gordon
|
|
|
|
|
\item Leo White
|
|
|
|
|
\item Andreas Rossberg
|
|
|
|
|
\item Robert Atkey
|
|
|
|
|
\item Jeremy Yallop
|
|
|
|
|
\item Simon Fowler
|
|
|
|
|
\item Craig McLaughlin
|
|
|
|
|
\item Garrett Morris
|
|
|
|
|
\item James McKinna
|
|
|
|
|
\item Brian Campbell
|
|
|
|
|
\item Paul Piho
|
|
|
|
|
\item Amna Shahab
|
|
|
|
|
\item Gordon Plotkin
|
|
|
|
|
\item Ohad Kammar
|
|
|
|
|
\item School of Informatics (funding)
|
|
|
|
|
\item Google (Kevin Millikin, Dmitry Stefantsov)
|
|
|
|
|
\end{itemize}
|
|
|
|
|
\end{acknowledgements}
|
|
|
|
|
|
|
|
|
|
%% Next we need to have the declaration.
|
|
|
|
|
%\standarddeclaration
|
|
|
|
|
\begin{declaration}
|
|
|
|
|
I declare that this thesis was composed by myself, that the work
|
|
|
|
|
contained herein is my own except where explicitly stated
|
|
|
|
|
otherwise in the text, and that this work has not been submitted
|
|
|
|
|
for any other degree or professional qualification except as
|
|
|
|
|
specified.
|
|
|
|
|
\end{declaration}
|
|
|
|
|
|
|
|
|
|
%% Finally, a dedication (this is optional -- uncomment the following line if
|
|
|
|
|
%% you want one).
|
|
|
|
|
% \dedication{To my mummy.}
|
|
|
|
|
\dedication{\emph{To everyone}}
|
|
|
|
|
|
|
|
|
|
% \begin{preface}
|
|
|
|
|
% A preface will possibly appear here\dots
|
|
|
|
|
% \end{preface}
|
|
|
|
|
|
|
|
|
|
%% Create the table of contents
|
|
|
|
|
\setcounter{secnumdepth}{2} % Numbering on sections and subsections
|
|
|
|
|
\setcounter{tocdepth}{1} % Show chapters, sections and subsections in TOC
|
|
|
|
|
%\singlespace
|
|
|
|
|
\tableofcontents
|
|
|
|
|
%\doublespace
|
|
|
|
|
|
|
|
|
|
%% If you want a list of figures or tables, uncomment the appropriate line(s)
|
|
|
|
|
% \listoffigures
|
|
|
|
|
% \listoftables
|
|
|
|
|
\end{preliminary}
|
|
|
|
|
|
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
|
%% Main content %%
|
|
|
|
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
|
|
|
|
|
|
|
|
|
|
%%
|
|
|
|
|
%% Introduction
|
|
|
|
|
%%
|
|
|
|
|
\chapter{Introduction}
|
|
|
|
|
\label{ch:introduction}
|
|
|
|
|
An enthralling introduction\dots
|
|
|
|
|
|
|
|
|
|
\section{Thesis outline}
|
|
|
|
|
Thesis outline\dots
|
|
|
|
|
|
|
|
|
|
\section{Typographical conventions}
|
|
|
|
|
Explain conventions\dots
|
|
|
|
|
|
|
|
|
|
\section{State of effectful programming}
|
|
|
|
|
Related work\dots
|
|
|
|
|
|
|
|
|
|
\chapter{Background}
|
|
|
|
|
\label{ch:background}
|
|
|
|
|
|
|
|
|
|
\chapter{A Core Calculus of Handlers and Rows}
|
|
|
|
|
\label{ch:language}
|
|
|
|
|
\section{Syntax}
|
|
|
|
|
\section{Static semantics}
|
|
|
|
|
\section{Dynamic semantics}
|
|
|
|
|
|
|
|
|
|
\chapter{Operational Foundations for Effect Handlers}
|
|
|
|
|
\label{ch:foundations}
|
|
|
|
|
\section{First-order continuation-passing style for deep handlers}
|
|
|
|
|
\section{Higher-order continuation-passing style for deep handlers}
|
|
|
|
|
\section{Continuation-passing style for effect handlers via generalised continuations}
|
|
|
|
|
\section{Abstract machine semantics for effect handlers via generalised continuations}
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
\chapter{On the Expressive Power of Effect Handlers}
|
|
|
|
|
\label{ch:expressiveness}
|
|
|
|
|
\section{Notions of expressiveness}
|
|
|
|
|
Fellesein's macro-expressiveness, Longley's type-respecting
|
|
|
|
|
expressiveness, Kammar's typability-preserving expressiveness.
|
|
|
|
|
|
|
|
|
|
\section{Interdefinability of deep and shallow handlers}
|
|
|
|
|
\section{The false allure of parameterised handlers}
|
|
|
|
|
|
|
|
|
|
\section{The fundamental efficiency of effect handlers}
|
|
|
|
|
|
|
|
|
|
\chapter{Related work}
|
|
|
|
|
\label{ch:related-work}
|
|
|
|
|
|
|
|
|
|
\chapter{Conclusions}
|
|
|
|
|
\label{ch:conclusions}
|
|
|
|
|
Some profound conclusions\dots
|
|
|
|
|
|
|
|
|
|
%%
|
|
|
|
|
%% Appendices
|
|
|
|
|
%%
|
|
|
|
|
% \appendix
|
|
|
|
|
|
|
|
|
|
%% If you want the bibliography single-spaced (which is allowed), uncomment
|
|
|
|
|
%% the next line.
|
|
|
|
|
%\nocite{*}
|
|
|
|
|
\singlespace
|
|
|
|
|
\nocite{*}
|
|
|
|
|
%\printbibliography[heading=bibintoc]
|
|
|
|
|
\bibliographystyle{unsrt}
|
|
|
|
|
\bibliography{\jobname}
|
|
|
|
|
|
|
|
|
|
%% ... that's all, folks!
|
|
|
|
|
\end{document}
|