My PhD dissertation at the University of Edinburgh, Scotland https://www.dhil.net/research/
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

271 lines
7.5 KiB

8 years ago
%% 12pt font size, PhD thesis, LFCS, print twosided, new chapters on right page
\documentclass[11pt,phd,lfcs,twoside,openright,logo,leftchapter,normalheadings]{infthesis}
8 years ago
\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[activate=true,
final,
tracking=true,
kerning=true,
spacing=true,
factor=1100,
stretch=10,
shrink=10]{microtype}
8 years ago
\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}
6 years ago
\SetProtrusion{encoding={*},family={bch},series={*},size={6,7}}
{1={ ,750},2={ ,500},3={ ,500},4={ ,500},5={ ,500},
6={ ,500},7={ ,600},8={ ,500},9={ ,500},0={ ,500}}
\SetExtraKerning[unit=space]
{encoding={*}, family={bch}, series={*}, size={footnotesize,small,normalsize}}
{\textendash={400,400}, % en-dash, add more space around it
"28={ ,150}, % left bracket, add space from right
"29={150, }, % right bracket, add space from left
\textquotedblleft={ ,150}, % left quotation mark, space from right
\textquotedblright={150, }} % right quotation mark, space from left
8 years ago
%% Information about the title, etc.
% \title{Higher-Order Theories of Handlers for Algebraic Effects}
% \title{Handlers for Algebraic Effects: Applications, Compilation, and Expressiveness}
% \title{Applications, Compilation, and Expressiveness for Effect Handlers}
% \title{Handling Computational Effects}
6 years ago
% \title{Programming Computable Effectful Functions}
% \title{Handling Effectful Computations}
\title{Foundations for Programming and Implementing Effect Handlers}
8 years ago
\author{Daniel Hillerström}
%% If the year of submission is not the current year, uncomment this line and
8 years ago
%% 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)
\item Microsoft Research (Daan Leijen)
8 years ago
\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}
8 years ago
%% Finally, a dedication (this is optional -- uncomment the following line if
%% you want one).
% \dedication{To my mummy.}
\dedication{\emph{To be or to do}}
8 years ago
% \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
%
Motivation: 1) compiler perspective: unifying control abstraction,
lean runtime, desugaring of async/await, generators/iterators, 2)
giving control to programmers, safer microkernels, everything as a
library.
8 years ago
\section{Thesis outline}
Thesis outline\dots
\section{Typographical conventions}
Explain conventions\dots
\part{Background}
\label{p:background}
\chapter{The State of Effectful Programming}
\label{ch:related-work}
\section{Type and Effect Systems}
\section{Monadic Programming}
\chapter{Continuations}
\label{ch:continuations}
\section{Zoo of Control Operators}
Describe how effect handlers fit amongst shift/reset, prompt/control,
callcc, J, catchcont, etc.
\section{Implementation Strategies}
\part{Design}
\chapter{A ML-like Base Language}
\section{Syntax and Static Semantics}
\section{Type Inference}
\section{Dynamic Semantics}
\chapter{Unary Handlers}
\label{ch:deep-handlers}
\section{Deep Handlers}
\subsection{Syntax and Static Semantics}
\subsection{Effect inference}
\subsection{Dynamic Semantics}
\section{Parameterised Handlers}
\section{Shallow Handlers}
\label{ch:shallow-handlers}
\subsection{Syntax and Static Semantics}
\subsection{Dynamic Semantics}
\chapter{N-ary Handlers}
\label{ch:multi-handlers}
% \section{Syntax and Static Semantics}
% \section{Dynamic Semantics}
\section{Unifying Deep and Shallow Handlers}
\part{Implementation}
\chapter{Continuation Passing Styles}
\chapter{Abstract Machine Semantics}
\part{Expressiveness}
\chapter{Computability, Complexity, and Expressivness}
\label{ch:expressiveness}
\section{Notions of Expressiveness}
Felleisen's macro-expressiveness, Longley's type-respecting
expressiveness, Kammar's typability-preserving expressiveness.
\section{Interdefinability of Deep and Shallow Handlers}
\section{Encoding Parameterised Handlers}
\chapter{The Asymptotic Power of Control}
\label{ch:handlers-efficiency}
Describe the methodology\dots
\section{Generic Search}
\section{Calculi}
\subsection{Base calculus}
\subsection{Handler calculus}
\section{A Practical Model of Computation}
\subsection{Syntax}
\subsection{Semantics}
\subsection{Realisability}
\section{Points, Predicates, and their Models}
\section{Efficient Generic Search with Effect Handlers}
\subsection{Space complexity}
\section{Best-case Complexity of Generic Search without Control}
\subsection{No shortcuts}
\subsection{No sharing}
\chapter{Robustness of the Asymptotic Power of Control}
\section{Mutable State}
\section{Exception Handling}
\section{Effect System}
\part{Conclusions}
\chapter{Conclusions}
8 years ago
\label{ch:conclusions}
Some profound conclusions\dots
\chapter{Future Work}
\label{ch:future-work}
8 years ago
%%
%% 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}