From f6b009a3c274cb5da56f3f6b29dd7f3de8c352d7 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Mon, 2 Jul 2018 18:14:46 +0100 Subject: [PATCH] Initial set-up --- pkgs/mathpartir.sty | 446 +++++++++++++++++++++++++++ pkgs/mathwidth.sty | 28 ++ thesis.bib | 728 ++++++++++++++++++++++++++++++++++++++++++++ thesis.tex | 143 +++++++++ 4 files changed, 1345 insertions(+) create mode 100644 pkgs/mathpartir.sty create mode 100644 pkgs/mathwidth.sty create mode 100644 thesis.bib create mode 100644 thesis.tex diff --git a/pkgs/mathpartir.sty b/pkgs/mathpartir.sty new file mode 100644 index 0000000..a39595a --- /dev/null +++ b/pkgs/mathpartir.sty @@ -0,0 +1,446 @@ +% Mathpartir --- Math Paragraph for Typesetting Inference Rules +% +% Copyright (C) 2001, 2002, 2003, 2004, 2005 Didier Rémy +% +% Author : Didier Remy +% Version : 1.2.0 +% Bug Reports : to author +% Web Site : http://pauillac.inria.fr/~remy/latex/ +% +% Mathpartir is free software; you can redistribute it and/or modify +% it under the terms of the GNU General Public License as published by +% the Free Software Foundation; either version 2, or (at your option) +% any later version. +% +% Mathpartir is distributed in the hope that it will be useful, +% but WITHOUT ANY WARRANTY; without even the implied warranty of +% MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +% GNU General Public License for more details +% (http://pauillac.inria.fr/~remy/license/GPL). +% +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% +% File mathpartir.sty (LaTeX macros) +%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% + +\NeedsTeXFormat{LaTeX2e} +\ProvidesPackage{mathpartir} + [2005/12/20 version 1.2.0 Math Paragraph for Typesetting Inference Rules] + +%% + +%% Identification +%% Preliminary declarations + +\RequirePackage {keyval} + +%% Options +%% More declarations + +%% PART I: Typesetting maths in paragraphe mode + +%% \newdimen \mpr@tmpdim +%% Dimens are a precious ressource. Uses seems to be local. +\let \mpr@tmpdim \@tempdima + +% To ensure hevea \hva compatibility, \hva should expands to nothing +% in mathpar or in inferrule +\let \mpr@hva \empty + +%% normal paragraph parametters, should rather be taken dynamically +\def \mpr@savepar {% + \edef \MathparNormalpar + {\noexpand \lineskiplimit \the\lineskiplimit + \noexpand \lineskip \the\lineskip}% + } + +\def \mpr@rulelineskip {\lineskiplimit=0.3em\lineskip=0.2em plus 0.1em} +\def \mpr@lesslineskip {\lineskiplimit=0.6em\lineskip=0.5em plus 0.2em} +\def \mpr@lineskip {\lineskiplimit=1.2em\lineskip=1.2em plus 0.2em} +\let \MathparLineskip \mpr@lineskip +\def \mpr@paroptions {\MathparLineskip} +\let \mpr@prebindings \relax + +\newskip \mpr@andskip \mpr@andskip 2em plus 0.5fil minus 0.5em + +\def \mpr@goodbreakand + {\hskip -\mpr@andskip \penalty -1000\hskip \mpr@andskip} +\def \mpr@and {\hskip \mpr@andskip} +\def \mpr@andcr {\penalty 50\mpr@and} +\def \mpr@cr {\penalty -10000\mpr@and} +\def \mpr@eqno #1{\mpr@andcr #1\hskip 0em plus -1fil \penalty 10} + +\def \mpr@bindings {% + \let \and \mpr@andcr + \let \par \mpr@andcr + \let \\\mpr@cr + \let \eqno \mpr@eqno + \let \hva \mpr@hva + } +\let \MathparBindings \mpr@bindings + +% \@ifundefined {ignorespacesafterend} +% {\def \ignorespacesafterend {\aftergroup \ignorespaces} + +\newenvironment{mathpar}[1][] + {$$\mpr@savepar \parskip 0em \hsize \linewidth \centering + \vbox \bgroup \mpr@prebindings \mpr@paroptions #1\ifmmode $\else + \noindent $\displaystyle\fi + \MathparBindings} + {\unskip \ifmmode $\fi\egroup $$\ignorespacesafterend} + +\newenvironment{mathparpagebreakable}[1][] + {\begingroup + \par + \mpr@savepar \parskip 0em \hsize \linewidth \centering + \mpr@prebindings \mpr@paroptions #1% + \vskip \abovedisplayskip \vskip -\lineskip% + \ifmmode \else $\displaystyle\fi + \MathparBindings + } + {\unskip + \ifmmode $\fi \par\endgroup + \vskip \belowdisplayskip + \noindent + \ignorespacesafterend} + +% \def \math@mathpar #1{\setbox0 \hbox {$\displaystyle #1$}\ifnum +% \wd0 < \hsize $$\box0$$\else \bmathpar #1\emathpar \fi} + +%%% HOV BOXES + +\def \mathvbox@ #1{\hbox \bgroup \mpr@normallineskip + \vbox \bgroup \tabskip 0em \let \\ \cr + \halign \bgroup \hfil $##$\hfil\cr #1\crcr \egroup \egroup + \egroup} + +\def \mathhvbox@ #1{\setbox0 \hbox {\let \\\qquad $#1$}\ifnum \wd0 < \hsize + \box0\else \mathvbox {#1}\fi} + + +%% Part II -- operations on lists + +\newtoks \mpr@lista +\newtoks \mpr@listb + +\long \def\mpr@cons #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter +{#2}\edef #2{\the \mpr@lista \the \mpr@listb}} + +\long \def\mpr@snoc #1\mpr@to#2{\mpr@lista {\\{#1}}\mpr@listb \expandafter +{#2}\edef #2{\the \mpr@listb\the\mpr@lista}} + +\long \def \mpr@concat#1=#2\mpr@to#3{\mpr@lista \expandafter {#2}\mpr@listb +\expandafter {#3}\edef #1{\the \mpr@listb\the\mpr@lista}} + +\def \mpr@head #1\mpr@to #2{\expandafter \mpr@head@ #1\mpr@head@ #1#2} +\long \def \mpr@head@ #1#2\mpr@head@ #3#4{\def #4{#1}\def#3{#2}} + +\def \mpr@flatten #1\mpr@to #2{\expandafter \mpr@flatten@ #1\mpr@flatten@ #1#2} +\long \def \mpr@flatten@ \\#1\\#2\mpr@flatten@ #3#4{\def #4{#1}\def #3{\\#2}} + +\def \mpr@makelist #1\mpr@to #2{\def \mpr@all {#1}% + \mpr@lista {\\}\mpr@listb \expandafter {\mpr@all}\edef \mpr@all {\the + \mpr@lista \the \mpr@listb \the \mpr@lista}\let #2\empty + \def \mpr@stripof ##1##2\mpr@stripend{\def \mpr@stripped{##2}}\loop + \mpr@flatten \mpr@all \mpr@to \mpr@one + \expandafter \mpr@snoc \mpr@one \mpr@to #2\expandafter \mpr@stripof + \mpr@all \mpr@stripend + \ifx \mpr@stripped \empty \let \mpr@isempty 0\else \let \mpr@isempty 1\fi + \ifx 1\mpr@isempty + \repeat +} + +\def \mpr@rev #1\mpr@to #2{\let \mpr@tmp \empty + \def \\##1{\mpr@cons ##1\mpr@to \mpr@tmp}#1\let #2\mpr@tmp} + +%% Part III -- Type inference rules + +\newif \if@premisse +\newbox \mpr@hlist +\newbox \mpr@vlist +\newif \ifmpr@center \mpr@centertrue +\def \mpr@htovlist {% + \setbox \mpr@hlist + \hbox {\strut + \ifmpr@center \hskip -0.5\wd\mpr@hlist\fi + \unhbox \mpr@hlist}% + \setbox \mpr@vlist + \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist + \else \unvbox \mpr@vlist \box \mpr@hlist + \fi}% +} +% OLD version +% \def \mpr@htovlist {% +% \setbox \mpr@hlist +% \hbox {\strut \hskip -0.5\wd\mpr@hlist \unhbox \mpr@hlist}% +% \setbox \mpr@vlist +% \vbox {\if@premisse \box \mpr@hlist \unvbox \mpr@vlist +% \else \unvbox \mpr@vlist \box \mpr@hlist +% \fi}% +% } + +\def \mpr@item #1{$\displaystyle #1$} +\def \mpr@sep{2em} +\def \mpr@blank { } +\def \mpr@hovbox #1#2{\hbox + \bgroup + \ifx #1T\@premissetrue + \else \ifx #1B\@premissefalse + \else + \PackageError{mathpartir} + {Premisse orientation should either be T or B} + {Fatal error in Package}% + \fi \fi + \def \@test {#2}\ifx \@test \mpr@blank\else + \setbox \mpr@hlist \hbox {}% + \setbox \mpr@vlist \vbox {}% + \if@premisse \let \snoc \mpr@cons \else \let \snoc \mpr@snoc \fi + \let \@hvlist \empty \let \@rev \empty + \mpr@tmpdim 0em + \expandafter \mpr@makelist #2\mpr@to \mpr@flat + \if@premisse \mpr@rev \mpr@flat \mpr@to \@rev \else \let \@rev \mpr@flat \fi + \def \\##1{% + \def \@test {##1}\ifx \@test \empty + \mpr@htovlist + \mpr@tmpdim 0em %%% last bug fix not extensively checked + \else + \setbox0 \hbox{\mpr@item {##1}}\relax + \advance \mpr@tmpdim by \wd0 + %\mpr@tmpdim 1.02\mpr@tmpdim + \ifnum \mpr@tmpdim < \hsize + \ifnum \wd\mpr@hlist > 0 + \if@premisse + \setbox \mpr@hlist + \hbox {\unhbox0 \hskip \mpr@sep \unhbox \mpr@hlist}% + \else + \setbox \mpr@hlist + \hbox {\unhbox \mpr@hlist \hskip \mpr@sep \unhbox0}% + \fi + \else + \setbox \mpr@hlist \hbox {\unhbox0}% + \fi + \else + \ifnum \wd \mpr@hlist > 0 + \mpr@htovlist + \mpr@tmpdim \wd0 + \fi + \setbox \mpr@hlist \hbox {\unhbox0}% + \fi + \advance \mpr@tmpdim by \mpr@sep + \fi + }% + \@rev + \mpr@htovlist + \ifmpr@center \hskip \wd\mpr@vlist\fi \box \mpr@vlist + \fi + \egroup +} + +%%% INFERENCE RULES + +\@ifundefined{@@over}{% + \let\@@over\over % fallback if amsmath is not loaded + \let\@@overwithdelims\overwithdelims + \let\@@atop\atop \let\@@atopwithdelims\atopwithdelims + \let\@@above\above \let\@@abovewithdelims\abovewithdelims + }{} + +%% The default + +\def \mpr@@fraction #1#2{\hbox {\advance \hsize by -0.5em + $\displaystyle {#1\mpr@over #2}$}} +\def \mpr@@nofraction #1#2{\hbox {\advance \hsize by -0.5em + $\displaystyle {#1\@@atop #2}$}} + +\let \mpr@fraction \mpr@@fraction + +%% A generic solution to arrow + +\def \mpr@make@fraction #1#2#3#4#5{\hbox {% + \def \mpr@tail{#1}% + \def \mpr@body{#2}% + \def \mpr@head{#3}% + \setbox1=\hbox{$#4$}\setbox2=\hbox{$#5$}% + \setbox3=\hbox{$\mkern -3mu\mpr@body\mkern -3mu$}% + \setbox3=\hbox{$\mkern -3mu \mpr@body\mkern -3mu$}% + \dimen0=\dp1\advance\dimen0 by \ht3\relax\dp1\dimen0\relax + \dimen0=\ht2\advance\dimen0 by \dp3\relax\ht2\dimen0\relax + \setbox0=\hbox {$\box1 \@@atop \box2$}% + \dimen0=\wd0\box0 + \box0 \hskip -\dimen0\relax + \hbox to \dimen0 {$% + \mathrel{\mpr@tail}\joinrel + \xleaders\hbox{\copy3}\hfil\joinrel\mathrel{\mpr@head}% + $}}} + +%% Old stuff should be removed in next version +\def \mpr@@nothing #1#2 + {$\lower 0.01pt \mpr@@nofraction {#1}{#2}$} +\def \mpr@@reduce #1#2{\hbox + {$\lower 0.01pt \mpr@@fraction {#1}{#2}\mkern -15mu\rightarrow$}} +\def \mpr@@rewrite #1#2#3{\hbox + {$\lower 0.01pt \mpr@@fraction {#2}{#3}\mkern -8mu#1$}} +\def \mpr@infercenter #1{\vcenter {\mpr@hovbox{T}{#1}}} + +\def \mpr@empty {} +\def \mpr@inferrule + {\bgroup + \ifnum \linewidth<\hsize \hsize \linewidth\fi + \mpr@rulelineskip + \let \and \qquad + \let \hva \mpr@hva + \let \@rulename \mpr@empty + \let \@rule@options \mpr@empty + \let \mpr@over \@@over + \mpr@inferrule@} +\newcommand {\mpr@inferrule@}[3][] + {\everymath={\displaystyle}% + \def \@test {#2}\ifx \empty \@test + \setbox0 \hbox {$\vcenter {\mpr@hovbox{B}{#3}}$}% + \else + \def \@test {#3}\ifx \empty \@test + \setbox0 \hbox {$\vcenter {\mpr@hovbox{T}{#2}}$}% + \else + \setbox0 \mpr@fraction {\mpr@hovbox{T}{#2}}{\mpr@hovbox{B}{#3}}% + \fi \fi + \def \@test {#1}\ifx \@test\empty \box0 + \else \vbox +%%% Suggestion de Francois pour les etiquettes longues +%%% {\hbox to \wd0 {\RefTirName {#1}\hfil}\box0}\fi + {\hbox {\RefTirName {#1}}\box0}\fi + \egroup} + +\def \mpr@vdotfil #1{\vbox to #1{\leaders \hbox{$\cdot$} \vfil}} + +% They are two forms +% \inferrule [label]{[premisses}{conclusions} +% or +% \inferrule* [options]{[premisses}{conclusions} +% +% Premisses and conclusions are lists of elements separated by \\ +% Each \\ produces a break, attempting horizontal breaks if possible, +% and vertical breaks if needed. +% +% An empty element obtained by \\\\ produces a vertical break in all cases. +% +% The former rule is aligned on the fraction bar. +% The optional label appears on top of the rule +% The second form to be used in a derivation tree is aligned on the last +% line of its conclusion +% +% The second form can be parameterized, using the key=val interface. The +% folloiwng keys are recognized: +% +% width set the width of the rule to val +% narrower set the width of the rule to val\hsize +% before execute val at the beginning/left +% lab put a label [Val] on top of the rule +% lskip add negative skip on the right +% left put a left label [Val] +% Left put a left label [Val], ignoring its width +% right put a right label [Val] +% Right put a right label [Val], ignoring its width +% leftskip skip negative space on the left-hand side +% rightskip skip negative space on the right-hand side +% vdots lift the rule by val and fill vertical space with dots +% after execute val at the end/right +% +% Note that most options must come in this order to avoid strange +% typesetting (in particular leftskip must preceed left and Left and +% rightskip must follow Right or right; vdots must come last +% or be only followed by rightskip. +% + +%% Keys that make sence in all kinds of rules +\def \mprset #1{\setkeys{mprset}{#1}} +\define@key {mprset}{andskip}[]{\mpr@andskip=#1} +\define@key {mprset}{lineskip}[]{\lineskip=#1} +\define@key {mprset}{flushleft}[]{\mpr@centerfalse} +\define@key {mprset}{center}[]{\mpr@centertrue} +\define@key {mprset}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} +\define@key {mprset}{atop}[]{\let \mpr@fraction \mpr@@nofraction} +\define@key {mprset}{myfraction}[]{\let \mpr@fraction #1} +\define@key {mprset}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} +\define@key {mprset}{sep}{\def\mpr@sep{#1}} + +\newbox \mpr@right +\define@key {mpr}{flushleft}[]{\mpr@centerfalse} +\define@key {mpr}{center}[]{\mpr@centertrue} +\define@key {mpr}{rewrite}[]{\let \mpr@fraction \mpr@@rewrite} +\define@key {mpr}{myfraction}[]{\let \mpr@fraction #1} +\define@key {mpr}{fraction}[]{\def \mpr@fraction {\mpr@make@fraction #1}} +\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax + \advance \hsize by -\wd0\box0} +\define@key {mpr}{width}{\hsize #1} +\define@key {mpr}{sep}{\def\mpr@sep{#1}} +\define@key {mpr}{before}{#1} +\define@key {mpr}{lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}} +\define@key {mpr}{Lab}{\let \RefTirName \TirName \def \mpr@rulename {#1}} +\define@key {mpr}{narrower}{\hsize #1\hsize} +\define@key {mpr}{leftskip}{\hskip -#1} +\define@key {mpr}{reduce}[]{\let \mpr@fraction \mpr@@reduce} +\define@key {mpr}{rightskip} + {\setbox \mpr@right \hbox {\unhbox \mpr@right \hskip -#1}} +\define@key {mpr}{LEFT}{\setbox0 \hbox {$#1$}\relax + \advance \hsize by -\wd0\box0} +\define@key {mpr}{left}{\setbox0 \hbox {$\TirName {#1}\;$}\relax + \advance \hsize by -\wd0\box0} +\define@key {mpr}{Left}{\llap{$\TirName {#1}\;$}} +\define@key {mpr}{right} + {\setbox0 \hbox {$\;\TirName {#1}$}\relax \advance \hsize by -\wd0 + \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} +\define@key {mpr}{RIGHT} + {\setbox0 \hbox {$#1$}\relax \advance \hsize by -\wd0 + \setbox \mpr@right \hbox {\unhbox \mpr@right \unhbox0}} +\define@key {mpr}{Right} + {\setbox \mpr@right \hbox {\unhbox \mpr@right \rlap {$\;\TirName {#1}$}}} +\define@key {mpr}{vdots}{\def \mpr@vdots {\@@atop \mpr@vdotfil{#1}}} +\define@key {mpr}{after}{\edef \mpr@after {\mpr@after #1}} + +\newcommand \mpr@inferstar@ [3][]{\setbox0 + \hbox {\let \mpr@rulename \mpr@empty \let \mpr@vdots \relax + \setbox \mpr@right \hbox{}% + $\setkeys{mpr}{#1}% + \ifx \mpr@rulename \mpr@empty \mpr@inferrule {#2}{#3}\else + \mpr@inferrule [{\mpr@rulename}]{#2}{#3}\fi + \box \mpr@right \mpr@vdots$} + \setbox1 \hbox {\strut} + \@tempdima \dp0 \advance \@tempdima by -\dp1 + \raise \@tempdima \box0} + +\def \mpr@infer {\@ifnextchar *{\mpr@inferstar}{\mpr@inferrule}} +\newcommand \mpr@err@skipargs[3][]{} +\def \mpr@inferstar*{\ifmmode + \let \@do \mpr@inferstar@ + \else + \let \@do \mpr@err@skipargs + \PackageError {mathpartir} + {\string\inferrule* can only be used in math mode}{}% + \fi \@do} + + +%%% Exports + +% Envirnonment mathpar + +\let \inferrule \mpr@infer + +% make a short name \infer is not already defined +\@ifundefined {infer}{\let \infer \mpr@infer}{} + +\def \TirNameStyle #1{\small \textsc{#1}} +\def \tir@name #1{\hbox {\small \TirNameStyle{#1}}} +\let \TirName \tir@name +\let \DefTirName \TirName +\let \RefTirName \TirName + +%%% Other Exports + +% \let \listcons \mpr@cons +% \let \listsnoc \mpr@snoc +% \let \listhead \mpr@head +% \let \listmake \mpr@makelist + + + + +\endinput diff --git a/pkgs/mathwidth.sty b/pkgs/mathwidth.sty new file mode 100644 index 0000000..eb497c2 --- /dev/null +++ b/pkgs/mathwidth.sty @@ -0,0 +1,28 @@ +\def\fileversion{2e} +\def\filedate{98/11/04} +\NeedsTeXFormat{LaTeX2e} + +\ProvidesPackage{mathwidth}[{% + \filedate\space\fileversion\space mathwidth package}] + +\@ifpackageloaded{lucbr}{}{% + \DeclareMathVersion{hask} + \SetMathAlphabet{\mathrm}{hask}{\encodingdefault}{\rmdefault}{m}{n}% + \SetMathAlphabet{\mathbf}{hask}{\encodingdefault}{\rmdefault}{bx}{n}% + \SetMathAlphabet{\mathsf}{hask}{\encodingdefault}{\sfdefault}{m}{n}% + \DeclareSymbolFont{italics}{\encodingdefault}{\rmdefault}{m}{it}% + \DeclareSymbolFontAlphabet{\mathrm}{operators} + \DeclareSymbolFontAlphabet{\mathit}{letters} + \DeclareSymbolFontAlphabet{\mathcal}{symbols} + \DeclareSymbolFontAlphabet{\haskit}{italics} + \mathversion{hask} + } + +% This next bit looks remarkably similar to part of zed.sty. It's used +% to change the spacing so that identifiers look nicer... +\def\@setmcodes#1#2#3{{\count0=#1 \count1=#3 + \loop \global\mathcode\count0=\count1 \ifnum \count0<#2 + \advance\count0 by1 \advance\count1 by1 \repeat}} +\@setmcodes{`A}{`Z}{"7\hexnumber@\symitalics41} +\@setmcodes{`a}{`z}{"7\hexnumber@\symitalics61} + diff --git a/thesis.bib b/thesis.bib new file mode 100644 index 0000000..4d16e06 --- /dev/null +++ b/thesis.bib @@ -0,0 +1,728 @@ + + +# Daniel's master's thesis (initial implementation of handlers in Links) +@MastersThesis{Hillerstrom15, + author = {Daniel Hillerström}, + title = {Handlers for Algebraic Effects in {Links}}, + school = {School of Informatics, the University of Edinburgh}, + address = {Scotland}, + month = aug, + year = 2015 +} + +# Daniel's master's 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}, + school = {School of Informatics, the University of Edinburgh}, + address = {Scotland}, + optmonth = aug, + year = 2016, +} + +# OCaml handlers +@misc{DolanWSYM15, + title = {Effective Concurrency through Algebraic Effects}, + author = {Stephen Dolan and Leo White and {KC} Sivaramakrishnan and Jeremy Yallop and Anil Madhavapeddy}, + year = 2015, + howpublished = {OCaml Workshop} +} + +@misc{DolanWM14, + title = {Multicore {OCaml}}, + author = {Stephen Dolan and Leo White and Anil Madhavapeddy}, + year = {2014}, + howpublished = {OCaml Workshop} +} + +@inproceedings{DolanEHMSW17, + author = {Stephen Dolan and + Spiros Eliopoulos and + Daniel Hillerstr{\"{o}}m and + Anil Madhavapeddy and + K. C. Sivaramakrishnan and + Leo White}, + title = {Concurrent System Programming with Effect Handlers}, + booktitle = {{TFP}}, + series = {Lecture Notes in Computer Science}, + volume = {10788}, + pages = {98--117}, + publisher = {Springer}, + year = {2017} +} + +# Efficient one-shot continuations +@inproceedings{BruggemanWD96, + author = {Carl Bruggeman and + Oscar Waddell and + R. Kent Dybvig}, + editor = {Charles N. Fischer}, + title = {Representing Control in the Presence of One-Shot Continuations}, + booktitle = {Proceedings of the {ACM} SIGPLAN'96 Conference on Programming Language + Design and Implementation (PLDI), Philadephia, Pennsylvania, May 21-24, + 1996}, + pages = {99--107}, + publisher = {{ACM}}, + year = {1996}, + OPTurl = {http://doi.acm.org/10.1145/231379.231395}, + OPTdoi = {10.1145/231379.231395}, + timestamp = {Mon, 21 May 2012 16:19:53 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/pldi/BruggemanWD96}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +# Links compiler + Multicore OCaml +@Misc{HillerstromLS16, + author = {Daniel Hillerström and Sam Lindley and KC Sivaramakrishnan}, + title = {Compiling {Links} Effect Handlers to the {OCaml} Backend}, + year = {2016}, + optmonth = sep, + howpublished = {{ML Workshop}} +} + +# Core references on handlers +@article{PlotkinP13, + author = {Gordon D. Plotkin and + Matija Pretnar}, + title = {Handling Algebraic Effects}, + journal = {Logical Methods in Computer Science}, + volume = {9}, + number = {4}, + year = {2013}, + OPTurl = {http://dx.doi.org/10.2168/LMCS-9(4:23)2013}, + OPTdoi = {10.2168/LMCS-9(4:23)2013}, + timestamp = {Thu, 31 Aug 4448958 16:06:56 +}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/corr/PlotkinP13}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{PlotkinP03, + author = {Gordon D. Plotkin and + John Power}, + title = {Algebraic Operations and Generic Effects}, + journal = {Applied Categorical Structures}, + volume = {11}, + number = {1}, + pages = {69--94}, + year = {2003}, + OPTurl = {http://dx.doi.org/10.1023/A:1023064908962}, + OPTdoi = {10.1023/A:1023064908962}, + timestamp = {Mon, 29 May 2006 12:06:44 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/acs/PlotkinP03}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{PlotkinP01, + author = {Gordon D. Plotkin and + John Power}, + title = {Adequacy for Algebraic Effects}, + booktitle = {FoSSaCS}, + OPTseries = {Lecture Notes in Computer Science}, + series = {LNCS}, + volume = {2030}, + pages = {1--24}, + publisher = {Springer}, + year = {2001} +} + +# Other algebraic effects and handlers +@InProceedings{Lindley14, + author = {Sam Lindley}, + editor = {Jos{\'{e}} Pedro Magalh{\~{a}}es and + Tiark Rompf}, + title = {Algebraic effects and effect handlers for idioms and arrows}, + booktitle = {Proceedings of the 10th {ACM} {SIGPLAN} workshop on Generic programming, + {WGP} 2014, Gothenburg, Sweden, August 31, 2014}, + pages = {47--58}, + publisher = {{ACM}}, + year = {2014}, + OPTurl = {http://doi.acm.org/10.1145/2633628.2633636}, + OPTdoi = {10.1145/2633628.2633636}, + timestamp = {Thu, 25 Jun 2015 13:50:37 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/icfp/Lindley14}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@article{Pretnar15, + author = {Matija Pretnar}, + title = {An Introduction to Algebraic Effects and Handlers}, + journal = {Electr. Notes Theor. Comput. Sci.}, + volume = {319}, + pages = {19--35}, + year = {2015}, + note = {Invited tutorial paper} +} + +@article{KammarP17, + author = {Ohad Kammar and Matija Pretnar}, + title = {No value restriction is needed for algebraic effects and handlers}, + journal = {Journal of Functional Programming}, + year = 2017, + OPTdoi = {https://doi.org/10.1017/S0956796816000320}, + volume = 27 +} + +@article{ForsterKLP17, + author = {Yannick Forster and + Ohad Kammar and + Sam Lindley and + Matija Pretnar}, + title = {On the Expressive Power of User-Defined Effects: Effect Handlers, + Monadic Reflection, Delimited Control}, + journal = {Proc. ACM Program. Lang.}, + volume = {1}, + number = {ICFP}, + articleno = {13}, + numpages = {29}, + month = sep, + year = {2017} +} + +# Eff +@article{BauerP15, + author = {Andrej Bauer and + Matija Pretnar}, + title = {Programming with algebraic effects and handlers}, + journal = {J. Log. Algebr. Meth. Program.}, + volume = {84}, + number = {1}, + pages = {108--123}, + year = {2015} +} + +# Idris +@inproceedings{Brady13, + author = {Edwin Brady}, + title = {Programming and reasoning with algebraic effects and dependent types}, + booktitle = {{ICFP}}, + pages = {133--144}, + publisher = {{ACM}}, + year = {2013} +} + +@inproceedings{Brady14, + author = {Edwin Brady}, + title = {Resource-Dependent Algebraic Effects}, + booktitle = {Trends in Functional Programming}, + OPTseries = {Lecture Notes in Computer Science}, + series = {LNCS}, + volume = {8843}, + pages = {18--33}, + publisher = {Springer}, + year = {2014} +} + +# Leo's HOPE talk +@misc{White16, + author = {Leo White}, + title = {Effective programming: bringing algebraic effects and handlers to {OCaml}}, + year = 2016, + optmonth = sep, + howpublished = {Keynote at {HOPE}, Nara, Japan} +} + +# Implementation of effect handlers in Links +@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} +} + +# Frank +@inproceedings{LindleyMM17, + author = {Sam Lindley and + Conor McBride and + Craig McLaughlin}, + title = {Do be do be do}, + booktitle = {{POPL}}, + pages = {500--514}, + publisher = {{ACM}}, + year = {2017} +} + +# Shonky +@misc{McBride16, + title={Shonky}, + author={Conor McBride}, + year=2016, + note={\url{https://github.com/pigworker/shonky}} +} + +# Koka +@inproceedings{Leijen14, + author = {Daan Leijen}, + title = {{Koka}: Programming with Row Polymorphic Effect Types}, + booktitle = {{MSFP}}, + series = {{EPTCS}}, + volume = {153}, + pages = {100--126}, + year = {2014} +} + +@inproceedings{Leijen17, + author = {Daan Leijen}, + title = {Type directed compilation of row-typed algebraic effects}, + booktitle = {{POPL}}, + pages = {486--499}, + publisher = {{ACM}}, + year = {2017} +} + +# Haskell implementations +@inproceedings{KiselyovSS13, + author = {Oleg Kiselyov and + Amr Sabry and + Cameron Swords}, + title = {Extensible effects: an alternative to monad transformers}, + booktitle = {Haskell}, + pages = {59--70}, + publisher = {{ACM}}, + year = {2013} +} + +@inproceedings{KiselyovI15, + author = {Oleg Kiselyov and + Hiromi Ishii}, + title = {Freer monads, more extensible effects}, + booktitle = {Haskell}, + pages = {94--105}, + publisher = {{ACM}}, + year = {2015} +} + + +@inproceedings{KammarLO13, + author = {Ohad Kammar and + Sam Lindley and + Nicolas Oury}, + title = {Handlers in action}, + booktitle = {{ICFP}}, + pages = {145--158}, + publisher = {{ACM}}, + year = {2013} +} + +@inproceedings{WuSH14, + author = {Nicolas Wu and + Tom Schrijvers and + Ralf Hinze}, + editor = {Wouter Swierstra}, + title = {Effect handlers in scope}, + booktitle = {Proceedings of the 2014 {ACM} {SIGPLAN} symposium on Haskell, Gothenburg, + Sweden, September 4-5, 2014}, + pages = {1--12}, + publisher = {{ACM}}, + year = {2014}, + url = {http://doi.acm.org/10.1145/2633357.2633358}, + doi = {10.1145/2633357.2633358}, + timestamp = {Mon, 08 Sep 2014 16:12:17 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/haskell/WuSH14}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +@inproceedings{WuS15, + author = {Nicolas Wu and + Tom Schrijvers}, + title = {Fusion for Free - Efficient Algebraic Effect Handlers}, + booktitle = {{MPC}}, + series = {Lecture Notes in Computer Science}, + volume = {9129}, + pages = {302--322}, + publisher = {Springer}, + year = {2015} +} + + +# Prolog +@article{SchrijversDDW13, + author = {Tom Schrijvers and + Bart Demoen and + Benoit Desouter and + Jan Wielemaker}, + title = {Delimited continuations for {Prolog}}, + journal = {{TPLP}}, + volume = {13}, + number = {4-5}, + pages = {533--546}, + year = {2013} +} + +@article{SalehS16, + author = {Amr Hany Saleh and + Tom Schrijvers}, + title = {Efficient Algebraic Effect Handlers for {Prolog}}, + journal = {{TPLP}}, + year = {2016}, + note = {Proceedings of {ICLP}} +} + +# References on Links +@inproceedings{CooperLWY06, + author = {Ezra Cooper and + Sam Lindley and + Philip Wadler and + Jeremy Yallop}, + title = {Links: Web Programming Without Tiers}, + booktitle = {{FMCO}}, + OPTseries = {Lecture Notes in Computer Science}, + series = {LNCS}, + volume = {4709}, + pages = {266--296}, + publisher = {Springer}, + year = {2006} +} + +@inproceedings{LindleyC12, + author = {Sam Lindley and + James Cheney}, + title = {Row-based effect types for database integration}, + booktitle = {{TLDI}}, + pages = {91--102}, + publisher = {{ACM}}, + year = {2012} +} + +# Monads +@article{Atkey09, + author = {Robert Atkey}, + title = {Parameterised notions of computation}, + journal = {Journal of Functional Programming}, + volume = {19}, + number = {3-4}, + pages = {335--376}, + year = {2009} +} + +@inproceedings{Moggi89, + author = {Eugenio Moggi}, + title = {Computational Lambda-Calculus and Monads}, + booktitle = {{LICS}}, + pages = {14--23}, + publisher = {{IEEE} Computer Society}, + year = {1989} +} + +@article{Moggi91, + author = {Eugenio Moggi}, + title = {Notions of Computation and Monads}, + journal = {Inf. Comput.}, + volume = {93}, + number = {1}, + pages = {55--92}, + year = {1991} +} + +@inproceedings{Wadler92, + author = {Philip Wadler}, + title = {The Essence of Functional Programming}, + booktitle = {{POPL}}, + pages = {1--14}, + publisher = {{ACM}}, + year = {1992} +} + +@inproceedings{Wadler95, + author = {Philip Wadler}, + title = {Monads for Functional Programming}, + booktitle = {Advanced Functional Programming}, + OPTseries = {Lecture Notes in Computer Science}, + series = {LNCS}, + volume = {925}, + pages = {24--52}, + publisher = {Springer}, + year = {1995} +} + +@article{Swierstra08, + author = {Wouter Swierstra}, + title = {Data types {\`{a}} la carte}, + journal = {Journal of Functional Programming}, + volume = {18}, + number = {4}, + pages = {423--436}, + year = {2008} +} + +# WebAssembly +@misc{HaasRSTGWBH17, + author = {Andreas Haas and Andreas Rossberg and Ben L. Titzer and Dan Gohman and Luke Wagner and JF Bastien and Michael Holman}, + title = {Bringing the {Web} up to Speed with {WebAssembly}}, + year = 2017, + note = {Draft}, + howpublished = {\url{https://people.mpi-sws.org/~rossberg/papers/Haas, Rossberg, Schuff, Titzer, Gohman, Wagner, Bastien, Holman - Bringing the Web up to Speed with WebAssembly [Draft].pdf}} +} + +# ECMAScript +@misc{EMCA15, + author = {{Ecma International}}, + title = {{ECMAScript} 2015 Language Specification}, + year = 2015, + url = {http://www.ecma-international.org/ecma-262/6.0/index.html} +} + +@misc{EMCA17, + author = {{Emca International}}, + title = {{ECMAScript} 2017 Language Specification}, + year = 2017, + url = {https://tc39.github.io/ecma262/} +} + +# Hop.js +@inproceedings{SerranoP16, + author = {Manuel Serrano and + Vincent Prunet}, + title = {A glimpse of Hopjs}, + booktitle = {{ICFP}}, + pages = {180--192}, + publisher = {{ACM}}, + year = {2016} +} + +# A-normal form +@inproceedings{FlanaganSDF93, + author = {Cormac Flanagan and + Amr Sabry and + Bruce F. Duba and + Matthias Felleisen}, + title = {The Essence of Compiling with Continuations}, + booktitle = {{PLDI}}, + pages = {237--247}, + publisher = {{ACM}}, + year = {1993} +} + +@inproceedings{SabryW96, + author = {Amr Sabry and + Philip Wadler}, + editor = {Robert Harper and + Richard L. Wexelblat}, + title = {A Reflection on Call-by-Value}, + booktitle = {Proceedings of the 1996 {ACM} {SIGPLAN} International Conference on + Functional Programming {(ICFP} '96), Philadelphia, Pennsylvania, May + 24-26, 1996.}, + pages = {13--24}, + publisher = {{ACM}}, + year = {1996}, + OPTurl = {http://doi.acm.org/10.1145/232627.232631}, + OPTdoi = {10.1145/232627.232631}, + timestamp = {Tue, 11 Jun 2013 13:54:16 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/conf/icfp/SabryW96}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + +# fine-grained call-by-value +@article{LevyPT03, + author = {Paul Blain Levy and + John Power and + Hayo Thielecke}, + title = {Modelling environments in call-by-value programming languages}, + journal = {Inf. Comput.}, + volume = {185}, + number = {2}, + pages = {182--210}, + year = {2003} +} + +# CPS +@article{Plotkin75, + author = {Gordon D. Plotkin}, + title = {Call-by-Name, Call-by-Value and the lambda-Calculus}, + journal = {Theor. Comput. Sci.}, + volume = {1}, + number = {2}, + pages = {125--159}, + year = {1975} +} + +@inproceedings{DanvyF90, + author = {Olivier Danvy and + Andrzej Filinski}, + title = {Abstracting Control}, + booktitle = {{LISP} and Functional Programming}, + pages = {151--160}, + year = {1990} +} + +@book{Appel92, + author = {Andrew W. Appel}, + title = {Compiling with Continuations}, + publisher = {Cambridge University Press}, + year = {1992} +} + +@article{DanvyN03, + author = {Olivier Danvy and + Lasse R. Nielsen}, + title = {A first-order one-pass {CPS} transformation}, + journal = {Theor. Comput. Sci.}, + volume = {308}, + number = {1-3}, + pages = {239--257}, + year = {2003} +} + +@inproceedings{Kennedy07, + author = {Andrew Kennedy}, + title = {Compiling with continuations, continued}, + booktitle = {{ICFP}}, + pages = {177--190}, + publisher = {{ACM}}, + year = {2007} +} + +@inproceedings{MaterzokB11, + author = {Marek Materzok and + Dariusz Biernacki}, + title = {Subtyping delimited continuations}, + booktitle = {{ICFP}}, + pages = {81--93}, + publisher = {{ACM}}, + year = {2011} +} + +@inproceedings{MaterzokB12, + author = {Marek Materzok and + Dariusz Biernacki}, + title = {A Dynamic Interpretation of the {CPS} Hierarchy}, + booktitle = {{APLAS}}, + OPTseries = {Lecture Notes in Computer Science}, + series = {LNCS}, + volume = {7705}, + pages = {296--311}, + publisher = {Springer}, + year = {2012} +} + +@Misc{KiselyovS16, + author = {Oleg Kiselyov and KC Sivaramakrishnan}, + title = {Eff directly in {OCaml}}, + year = {2016}, + optmonth = sep, + howpublished = {{ML Workshop}} +} + +% fancy row typing systems that support shapes +@inproceedings{BerthomieuS95, + author = {Bernard Berthomieu and Camille le Moniès de Sagazan}, + title = {A Calculus of Tagged Types, with applications to process languages}, + booktitle = {Workshop on Types for Program Analysis}, + year = 1995, +} + +@techreport{Remy93, + title = {{Syntactic theories and the algebra of record terms}}, + author = {Didier Remy}, + number = {RR-1869}, + institution = {{INRIA}}, + year = {1993}, +} + + + +@article{Huet97, + author = {G{\'{e}}rard P. Huet}, + title = {The Zipper}, + journal = {J. Funct. Program.}, + volume = {7}, + number = {5}, + pages = {549--554}, + year = {1997}, + OPTurl = {http://journals.cambridge.org/action/displayAbstract?aid=44121}, + timestamp = {Fri, 10 Jun 2011 14:42:10 +0200}, + biburl = {http://dblp.uni-trier.de/rec/bib/journals/jfp/Huet97}, + bibsource = {dblp computer science bibliography, http://dblp.org} +} + + + + +@article{Hughes00, + author = {John Hughes}, + title = {Generalising monads to arrows}, + journal = {Sci. Comput. Program.}, + volume = {37}, + number = {1-3}, + pages = {67--111}, + year = {2000} +} + + + +% CPS for effect handlers +@inproceedings{HillerstromLAS17, + author = {Daniel Hillerstr{\"{o}}m and + Sam Lindley and + Robert Atkey and + K. C. 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} +} + +% CEK +@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} +} + +@article{BiernackiPPS18, + author = {Dariusz Biernacki and + Maciej Pir{\'{o}}g and + Piotr Polesiuk and + Filip Sieczkowski}, + title = {Handle with care: relational interpretation of algebraic effects and + handlers}, + journal = {{PACMPL}}, + volume = {2}, + number = {{POPL}}, + pages = {8:1--8:30}, + year = {2018} +} + +% explicit effect subtyping +@inproceedings{SalehKPS18, + author = {Amr Hany Saleh and + Georgios Karachalias and + Matija Pretnar and + Tom Schrijvers}, + title = {Explicit Effect Subtyping}, + booktitle = {{ESOP}}, + series = {Lecture Notes in Computer Science}, + volume = {10801}, + pages = {327--354}, + publisher = {Springer}, + year = {2018} +} + +# Pyro +@Misc{Goodman17, + author = {Noah Goodman}, + title = {Uber {AI} {Labs} Open Sources {Pyro}, a Deep Probabilistic Programming Language}, + month = nov, + year = 2017, + url = {https://eng.uber.com/pyro/} +} + +# Meta programming +@article{Yallop17, + author = {Jeremy Yallop}, + title = {Staged generic programming}, + journal = {{PACMPL}}, + volume = {1}, + number = {{ICFP}}, + pages = {29:1--29:29}, + year = {2017} +} diff --git a/thesis.tex b/thesis.tex new file mode 100644 index 0000000..1a3d707 --- /dev/null +++ b/thesis.tex @@ -0,0 +1,143 @@ +%% 12pt font size, PhD thesis, LFCS, print twosided, new chapters on right page +\documentclass[12pt,phd,lfcs,twoside,openright,logo,rightchapter,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{Daniel's PhD Thesis} +\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 + \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{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 + +\chapter{Conclusions} +\label{ch:conclusions} +Some profound conclusions\dots + +%% +%% Appendices +%% +% \appendix +% \chapter{Installing the Links compiler} +% \label{ch:install} + +%% 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}