mirror of
https://github.com/dhil/phd-dissertation
synced 2026-03-12 18:48:25 +00:00
Initial set-up
This commit is contained in:
446
pkgs/mathpartir.sty
Normal file
446
pkgs/mathpartir.sty
Normal file
@@ -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
|
||||||
28
pkgs/mathwidth.sty
Normal file
28
pkgs/mathwidth.sty
Normal file
@@ -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}
|
||||||
|
|
||||||
728
thesis.bib
Normal file
728
thesis.bib
Normal file
@@ -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}
|
||||||
|
}
|
||||||
143
thesis.tex
Normal file
143
thesis.tex
Normal file
@@ -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}
|
||||||
Reference in New Issue
Block a user