Moved sbmf/sbmf to papers/sbmf and copied over for scp
This commit is contained in:
Wen Kokke
parent
cd5f1dd2d4
commit
48aea0854f
83 changed files with 9243 additions and 0 deletions
|
Before Width: | Height: | Size: 168 KiB After Width: | Height: | Size: 168 KiB |
|
Before Width: | Height: | Size: 105 KiB After Width: | Height: | Size: 105 KiB |
|
Before Width: | Height: | Size: 120 KiB After Width: | Height: | Size: 120 KiB |
|
Before Width: | Height: | Size: 148 KiB After Width: | Height: | Size: 148 KiB |
|
Before Width: | Height: | Size: 208 KiB After Width: | Height: | Size: 208 KiB |
|
Before Width: | Height: | Size: 135 KiB After Width: | Height: | Size: 135 KiB |
|
Before Width: | Height: | Size: 25 KiB After Width: | Height: | Size: 25 KiB |
|
Before Width: | Height: | Size: 240 KiB After Width: | Height: | Size: 240 KiB |
|
Before Width: | Height: | Size: 275 KiB After Width: | Height: | Size: 275 KiB |
|
Before Width: | Height: | Size: 211 KiB After Width: | Height: | Size: 211 KiB |
|
Before Width: | Height: | Size: 473 KiB After Width: | Height: | Size: 473 KiB |
|
Before Width: | Height: | Size: 360 KiB After Width: | Height: | Size: 360 KiB |
|
Before Width: | Height: | Size: 334 KiB After Width: | Height: | Size: 334 KiB |
|
Before Width: | Height: | Size: 36 KiB After Width: | Height: | Size: 36 KiB |
|
Before Width: | Height: | Size: 379 KiB After Width: | Height: | Size: 379 KiB |
|
Before Width: | Height: | Size: 260 KiB After Width: | Height: | Size: 260 KiB |
|
Before Width: | Height: | Size: 86 KiB After Width: | Height: | Size: 86 KiB |
20
papers/scp/Makefile
Normal file
20
papers/scp/Makefile
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
.PHONY : default %.pdf clean realclean
|
||||
.PRECIOUS : %.tex
|
||||
|
||||
default : PLFA.pdf
|
||||
|
||||
PLFA.pdf : PLFA.tex PLFA.bib
|
||||
pdflatex PLFA
|
||||
bibtex PLFA
|
||||
pdflatex PLFA
|
||||
bibtex PLFA
|
||||
pdflatex PLFA
|
||||
|
||||
final.zip : PLFA.tex PLFA.bib
|
||||
zip final.zip agda.sty llncs.cls PLFA.tex PLFA.bib splncsnat.bst figures/plfa-*.png figures/sf-*.png figures/raw.png figures/inherent.png
|
||||
|
||||
clean:
|
||||
rm -f *.aux *.log *.out *.ptb *.blg *.fdb_latexmk *.agdai *.fls
|
||||
|
||||
realclean: clean
|
||||
rm -f *.glob *.vo *.bbl latex/* PLFA.pdf
|
||||
286
papers/scp/PLFA.bib
Normal file
286
papers/scp/PLFA.bib
Normal file
|
|
@ -0,0 +1,286 @@
|
|||
@inproceedings{Allais-et-al-2017,
|
||||
title={Type-and-scope safe programs and their proofs},
|
||||
author={Allais, Guillaume and Chapman, James and McBride, Conor and McKinna, James},
|
||||
booktitle={Proceedings of the 6th ACM SIGPLAN Conference on Certified Programs and Proofs},
|
||||
pages={195--207},
|
||||
year={2017},
|
||||
organization={ACM}
|
||||
}
|
||||
|
||||
@inproceedings{Altenkirch-and-Reus-1999,
|
||||
title={Monadic presentations of lambda terms using generalized inductive types},
|
||||
author={Altenkirch, Thorsten and Reus, Bernhard},
|
||||
booktitle={International Workshop on Computer Science Logic},
|
||||
pages={453--468},
|
||||
year={1999},
|
||||
organization={Springer}
|
||||
}
|
||||
|
||||
@article{Avigad-and-Harrison-2014,
|
||||
title={Formally verified mathematics},
|
||||
author={Avigad, Jeremy and Harrison, John},
|
||||
journal={Communications of the ACM},
|
||||
volume={57},
|
||||
number={4},
|
||||
pages={66--75},
|
||||
year={2014},
|
||||
publisher={ACM}
|
||||
}
|
||||
|
||||
@inproceedings{Berger-1993,
|
||||
title={Program extraction from normalization proofs},
|
||||
author={Berger, Ulrich},
|
||||
booktitle={International Conference on Typed Lambda Calculi and Applications},
|
||||
pages={91--106},
|
||||
year={1993},
|
||||
organization={Springer}
|
||||
}
|
||||
|
||||
@inproceedings{Bove-and-Capretta-2001,
|
||||
title={Nested general recursion and partiality in type theory},
|
||||
author={Bove, Ana and Capretta, Venanzio},
|
||||
booktitle={International Conference on Theorem Proving in Higher Order Logics},
|
||||
pages={121--125},
|
||||
year={2001},
|
||||
organization={Springer}
|
||||
}
|
||||
|
||||
@inproceedings{Bove-et-al-2009,
|
||||
title={A brief overview of Agda--a functional language with dependent types},
|
||||
author={Bove, Ana and Dybjer, Peter and Norell, Ulf},
|
||||
booktitle={International Conference on Theorem Proving in Higher Order Logics},
|
||||
pages={73--78},
|
||||
year={2009},
|
||||
organization={Springer}
|
||||
}
|
||||
|
||||
@article{Capretta-2005,
|
||||
title={General recursion via coinductive types},
|
||||
author={Venanzio Capretta},
|
||||
journal={Logical Methods in Computer Science},
|
||||
volume={1},
|
||||
number={2},
|
||||
year={2005}
|
||||
}
|
||||
|
||||
@phdthesis{Chapman-2009,
|
||||
title={Type checking and normalisation},
|
||||
author={Chapman, James Maitland},
|
||||
year={2009},
|
||||
school={University of Nottingham}
|
||||
}
|
||||
|
||||
@inproceedings{Danas-et-al-2017,
|
||||
title={User Studies of Principled Model Finder Output},
|
||||
author={Danas, Natasha and Nelson, Tim and Harrison, Lane and Krishnamurthi, Shriram and Dougherty, Daniel J},
|
||||
booktitle={International Conference on Software Engineering and Formal Methods},
|
||||
pages={168--184},
|
||||
year={2017},
|
||||
organization={Springer}
|
||||
}
|
||||
|
||||
@inproceedings{Dagand-and-Scherer-2015,
|
||||
title={Normalization by realizability also evaluates},
|
||||
author={Dagand, Pierre-{\'E}variste and Scherer, Gabriel},
|
||||
booktitle={Vingt-sixi{\`e}mes Journ{\'e}es Francophones des Langages Applicatifs (JFLA 2015)},
|
||||
year={2015}
|
||||
}
|
||||
|
||||
@book {Felleisen-et-al-2009,
|
||||
title = {Semantics engineering with PLT Redex},
|
||||
author = {Felleisen, Matthias and Findler, Robert Bruce and Flatt, Matthew},
|
||||
year = {2009},
|
||||
publisher = {By Press}
|
||||
}
|
||||
|
||||
@techreport{Goguen-and-McKinna-1997,
|
||||
title={Candidates for substitution},
|
||||
author={Goguen, Healfdene and McKinna, James},
|
||||
institution={Laboratory for Foundations of Computer Science, University of Edinburgh},
|
||||
year={1997}
|
||||
}
|
||||
|
||||
@incollection{Gonthier-2008,
|
||||
title={The four colour theorem: Engineering of a formal proof},
|
||||
author={Gonthier, Georges},
|
||||
booktitle={Computer mathematics},
|
||||
pages={333--333},
|
||||
year={2008},
|
||||
publisher={Springer}
|
||||
}
|
||||
|
||||
@inproceedings{Gonthier-et-al-2013,
|
||||
title={A machine-checked proof of the odd order theorem},
|
||||
author={Gonthier, Georges and Asperti, Andrea and Avigad, Jeremy and others},
|
||||
booktitle={International Conference on Interactive Theorem Proving},
|
||||
pages={163--179},
|
||||
year={2013},
|
||||
organization={Springer}
|
||||
}
|
||||
|
||||
@inproceedings{Hales-et-al-2017,
|
||||
title={A formal proof of the {K}epler conjecture},
|
||||
author={Hales, Thomas and Adams, Mark and Bauer, Gertrud and Dang, Tat Dat and Harrison, John and Le Truong, Hoang and Kaliszyk, Cezary and Magron, Victor and McLaughlin, Sean and Nguyen, Tat Thang and others},
|
||||
booktitle={Forum of Mathematics, Pi},
|
||||
volume={5},
|
||||
year={2017},
|
||||
organization={Cambridge University Press}
|
||||
}
|
||||
|
||||
@book{Harper-2016,
|
||||
title={Practical foundations for programming languages},
|
||||
author={Harper, Robert},
|
||||
year={2016},
|
||||
publisher={Cambridge University Press}
|
||||
}
|
||||
|
||||
@article{Huet-et-al-1997,
|
||||
title={The {C}oq proof assistant a tutorial},
|
||||
author={Huet, G{\'e}rard and Kahn, Gilles and Paulin-Mohring, Christine},
|
||||
journal={Rapport Technique},
|
||||
volume={178},
|
||||
year={1997}
|
||||
}
|
||||
|
||||
@inproceedings{Kastner-et-al-2017,
|
||||
title={Closing the gap--the formally verified optimizing compiler CompCert},
|
||||
author={K{\"a}stner, Daniel and Leroy, Xavier and Blazy, Sandrine and Schommer, Bernhard and Schmidt, Michael and Ferdinand, Christian},
|
||||
booktitle={SSS'17: Safety-critical Systems Symposium 2017},
|
||||
pages={163--180},
|
||||
year={2017},
|
||||
organization={CreateSpace}
|
||||
}
|
||||
|
||||
@misc{Kiselyov-2009,
|
||||
author={Oleg Kiselyov},
|
||||
title={Formalizing languages, mechanizing type-soundess and other meta-theoretic proofs},
|
||||
note={unpublished manuscript},
|
||||
url={http://okmij.org/ftp/formalizations/index.html},
|
||||
year={2009}
|
||||
}
|
||||
|
||||
@inproceedings{Klein-2009,
|
||||
title={seL4: Formal verification of an OS kernel},
|
||||
author={Klein, Gerwin and Elphinstone, Kevin and Heiser, Gernot and Andronick, June and Cock, David and Derrin, Philip and Elkaduwe, Dhammika and Engelhardt, Kai and Kolanski, Rafal and Norrish, Michael and others},
|
||||
booktitle={Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles},
|
||||
pages={207--220},
|
||||
year={2009},
|
||||
organization={ACM}
|
||||
}
|
||||
|
||||
@article{Leroy-2009,
|
||||
title={Formal verification of a realistic compiler},
|
||||
author={Leroy, Xavier},
|
||||
journal={Communications of the ACM},
|
||||
volume={52},
|
||||
number={7},
|
||||
pages={107--115},
|
||||
year={2009},
|
||||
publisher={ACM}
|
||||
}
|
||||
|
||||
@misc{McBride-2005,
|
||||
title={Type-preserving renaming and substitution},
|
||||
author={McBride, Conor},
|
||||
note={unpublished manuscript},
|
||||
url={https://personal.cis.strath.ac.uk/conor.mcbride/ren-sub.pdf},
|
||||
year={2005}
|
||||
}
|
||||
|
||||
@inproceedings{McBride-2015,
|
||||
title={Turing-completeness totally free},
|
||||
author={McBride, Conor},
|
||||
booktitle={International Conference on Mathematics of Program Construction},
|
||||
pages={257--275},
|
||||
year={2015},
|
||||
organization={Springer}
|
||||
}
|
||||
|
||||
@article{McBride-and-McKinna-2004,
|
||||
title={The view from the left},
|
||||
author={McBride, Conor and McKinna, James},
|
||||
journal={Journal of functional programming},
|
||||
volume={14},
|
||||
number={1},
|
||||
pages={69--111},
|
||||
year={2004},
|
||||
publisher={Cambridge University Press}
|
||||
}
|
||||
|
||||
@inproceedings{O'Connor-2016,
|
||||
title={Refinement through restraint: Bringing down the cost of verification},
|
||||
author={O'Connor, Liam and Chen, Zilin and Rizkallah, Christine and Amani, Sidney and Lim, Japheth and Murray, Toby and Nagashima, Yutaka and Sewell, Thomas and Klein, Gerwin},
|
||||
booktitle={ICFP},
|
||||
pages={89--102},
|
||||
year={2016}
|
||||
}
|
||||
|
||||
@book{Pierce-2002,
|
||||
title={Types and programming languages},
|
||||
author={Pierce, Benjamin C},
|
||||
year={2002},
|
||||
publisher={MIT press}
|
||||
}
|
||||
|
||||
@inproceedings{Pierce-2009,
|
||||
title={Lambda, {T}he {U}ltimate {TA}},
|
||||
author={Pierce, Benjamin C},
|
||||
booktitle={ICFP},
|
||||
pages={121--22},
|
||||
year={2009}
|
||||
}
|
||||
|
||||
@book{Pierce-et-al-2010,
|
||||
title={Software foundations},
|
||||
author={Benjamin C Pierce and Chris Casinghino and Marco Gaboardi and Michael Greenberg and C{\u{a}}t{\u{a}}lin Hri{\c{t}}cu and Vilhelm Sj{\"o}berg and Brent Yorgey},
|
||||
url={http://www.cis.upenn.edu/bcpierce/sf/current/index.html},
|
||||
year={2010}
|
||||
}
|
||||
|
||||
@inproceedings{Pitts-2010,
|
||||
title={Step-indexed biorthogonality: a tutorial example},
|
||||
author={Pitts, Andrew M},
|
||||
booktitle={Dagstuhl Seminar Proceedings},
|
||||
year={2010},
|
||||
organization={Schloss Dagstuhl-Leibniz-Zentrum f{\~A}$1/4$r Informatik}
|
||||
}
|
||||
|
||||
@article{Plotkin-1977,
|
||||
title={LCF considered as a programming language},
|
||||
author={Plotkin, Gordon D.},
|
||||
journal={Theoretical Computer Science},
|
||||
volume={5},
|
||||
number={3},
|
||||
pages={223--255},
|
||||
year={1977},
|
||||
publisher={Elsevier}
|
||||
}
|
||||
|
||||
|
||||
@article{Rosu-Serbanuta-2010,
|
||||
title={An Overview of the {K} Semantic Framework},
|
||||
author={Grigore Ro{\c s}u and Traian Florin {\c S}erb{\u a}nu{\c t}{\u a} },
|
||||
journal={Journal of Logic and Algebraic Programming},
|
||||
volume={79},
|
||||
number={6},
|
||||
pages={397--434},
|
||||
year={2010}
|
||||
}
|
||||
|
||||
@book{Stump-2016,
|
||||
title={Verified functional programming in Agda},
|
||||
author={Stump, Aaron},
|
||||
year={2016},
|
||||
publisher={Morgan \& Claypool}
|
||||
}
|
||||
|
||||
@article{Wright-and-Felleisen-1994,
|
||||
title={A syntactic approach to type soundness},
|
||||
author={Wright, Andrew K and Felleisen, Matthias},
|
||||
journal={Information and computation},
|
||||
volume={115},
|
||||
number={1},
|
||||
pages={38--94},
|
||||
year={1994},
|
||||
publisher={San Diego: Academic Press, c1987-}
|
||||
}
|
||||
BIN
papers/scp/PLFA.pdf
Normal file
BIN
papers/scp/PLFA.pdf
Normal file
Binary file not shown.
740
papers/scp/PLFA.tex
Executable file
740
papers/scp/PLFA.tex
Executable file
|
|
@ -0,0 +1,740 @@
|
|||
%\documentclass[runningheads,oribibl]{llncs}
|
||||
\documentclass[runningheads]{llncs}
|
||||
\usepackage{natbib}
|
||||
% \usepackage{stmaryrd}
|
||||
% \usepackage{proof}
|
||||
% \usepackage{amsmath}
|
||||
% \usepackage{amssymb}
|
||||
% \usepackage{color}
|
||||
% \usepackage{bbm}
|
||||
% \usepackage[greek,english]{babel}
|
||||
% \usepackage{ucs}
|
||||
% \usepackage[utf8x]{inputenc}
|
||||
% \usepackage{autofe}
|
||||
\usepackage{agda}
|
||||
\usepackage{revsymb}
|
||||
\usepackage{semantic}
|
||||
\usepackage{graphicx}
|
||||
\usepackage{url}
|
||||
\renewcommand\UrlFont{\color{blue}\rmfamily}
|
||||
\usepackage{stix}
|
||||
\setcitestyle{round,aysep={}}
|
||||
|
||||
\begin{document}
|
||||
\title{Programming Language Foundations in Agda}
|
||||
\author{Philip Wadler}
|
||||
\authorrunning{P. Wadler}
|
||||
\institute{University of Edinburgh\\
|
||||
\email{wadler@inf.ed.ac.uk}}
|
||||
\maketitle
|
||||
%
|
||||
\begin{abstract}
|
||||
One of the leading textbooks for formal methods is
|
||||
\emph{Software Foundations} (SF), written by Benjamin Pierce in
|
||||
collaboration with others, and based on Coq. After five years using SF
|
||||
in the classroom, I have come to the conclusion that Coq is not the
|
||||
best vehicle for this purpose, as too much of the course needs to
|
||||
focus on learning tactics for proof derivation, to the cost of
|
||||
learning programming language theory. Accordingly, I have written a
|
||||
new textbook, \emph{Programming Language Foundations in Agda} (PLFA).
|
||||
PLFA covers much of the same ground as SF, although it is not a
|
||||
slavish imitation.
|
||||
|
||||
What did I learn from writing PLFA? First, that it is possible. One
|
||||
might expect that without proof tactics that the proofs become too
|
||||
long, but in fact proofs in PLFA are about the same length as those in
|
||||
SF. Proofs in Coq require an interactive environment to be understood,
|
||||
while proofs in Agda can be read on the page. Second, that
|
||||
constructive proofs of preservation and progress give immediate rise
|
||||
to a prototype evaluator. This fact is obvious in retrospect but it is
|
||||
not exploited in SF (which instead provides a separate normalise
|
||||
tactic) nor can I find it in the literature. Third, that using raw
|
||||
terms with a separate typing relation is far less perspicuous than
|
||||
using inherently-typed terms. SF uses the former presentation, while
|
||||
PLFA presents both; the former uses about 1.6 as many lines of Agda
|
||||
code as the latter, roughly the golden ratio.
|
||||
|
||||
The textbook is written as a literate Agda script, and can be found here:
|
||||
\begin{center}
|
||||
\url{http://plfa.inf.ed.ac.uk}
|
||||
\end{center}
|
||||
\keywords{Agda \and Coq \and lambda calculus \and dependent types.}
|
||||
\end{abstract}
|
||||
|
||||
\section{Introduction}
|
||||
|
||||
The most profound connection between logic and computation is a pun.
|
||||
The doctrine of Propositions as Types asserts that a certain kind of formal
|
||||
structure may be read in two ways: either as a proposition in logic or
|
||||
as a type in computing. Further, a related structure may be read as
|
||||
either the proof of the proposition or as a programme of the
|
||||
corresponding type. Further still, simplification of proofs
|
||||
corresponds to evaluation of programs.
|
||||
|
||||
Accordingly, the title of this paper, and the corresponding textbook,
|
||||
\emph{Programming Language Foundations in Agda} (hence, PLFA)
|
||||
also has two readings. It may be parsed as ``(Programming Language)
|
||||
Foundations in Agda'' or ``Programming (Language Foundations) in
|
||||
Agda''---specifications in the proof assistant Agda both describe
|
||||
programming languages and are themselves programmes.
|
||||
|
||||
Since 2013, I have taught a course on Types and Semantics for
|
||||
Programming Languages to fourth-year undergraduates and masters
|
||||
students at the University of Edinburgh. An earlier version of that
|
||||
course was based on \emph{Types and Programming Languages} by
|
||||
\citet{Pierce-2002}, but my version was taught from its successor,
|
||||
\emph{Software Foundations} (hence, SF) by \citet{Pierce-et-al-2010},
|
||||
which is based on the proof assistance Coq \citep{Huet-et-al-1997}.
|
||||
I am convinced by the claim of \citet{Pierce-2009}, made in his ICFP
|
||||
Keynote \emph{Lambda, The Ultimate TA}, that basing a course around a
|
||||
proof assistant aids learning.
|
||||
|
||||
However, after five years of experience, I have come to the conclusion
|
||||
that Coq is not the best vehicle. Too much of the course needs to
|
||||
focus on learning tactics for proof derivation, to the cost of
|
||||
learning the fundamentals of programming language theory. Every
|
||||
concept has to be learned twice: e.g., both the product data type, and
|
||||
the corresponding tactics for introduction and elimination of
|
||||
conjunctions. The rules Coq applies to generate induction hypotheses
|
||||
can sometimes seem mysterious. While the \texttt{notation} construct
|
||||
permits pleasingly flexible syntax, it can be confusing that the same
|
||||
concept must always be given two names, e.g., both
|
||||
\texttt{subst~N~x~M} and \texttt{N~[x~:=~M]}. Names of tactics are
|
||||
sometimes short and sometimes long; naming conventions in the standard
|
||||
library can be wildly inconsistent. \emph{Propositions as types} as a
|
||||
foundation of proof is present but hidden.
|
||||
|
||||
I found myself keen to recast the course in Agda \citep{Bove-et-al-2009}.
|
||||
In Agda, there is
|
||||
no longer any need to learn about tactics: there is just
|
||||
dependently-typed programming, plain and simple. Introduction is
|
||||
always by a constructor, elimination is always by pattern
|
||||
matching. Induction is no longer a mysterious separate concept, but
|
||||
corresponds to the familiar notion of recursion. Mixfix syntax is
|
||||
flexible while using just one name for each concept, e.g.,
|
||||
substitution is \texttt{\_[\_:=\_]}. The standard library is not perfect, but
|
||||
there is a fair attempt at consistency. \emph{Propositions as types} as a
|
||||
foundation of proof is on proud display.
|
||||
|
||||
Alas, there is no textbook for programming language theory in
|
||||
Agda. \emph{Verified Functional Programming in Agda} by \citep{Stump-2016}
|
||||
covers related ground, but focusses more on programming with dependent
|
||||
types than on the theory of programming languages.
|
||||
|
||||
The original goal was to simply adapt \emph{Software Foundations},
|
||||
maintaining the same text but transposing the code from Coq to Agda.
|
||||
But it quickly became clear to me that after five years in the
|
||||
classroom I had my own ideas about how to present the material. They
|
||||
say you should never write a book unless you cannot \emph{not} write the
|
||||
book, and I soon found that this was a book I could not not write.
|
||||
|
||||
I am fortunate that my student, Wen Kokke, was keen to help. She
|
||||
guided me as a newbie to Agda and provided an infrastructure that is
|
||||
easy to use and produces pages that are a pleasure to view.
|
||||
The bulk of the book was written January--June 2018, while on
|
||||
sabbatical in Rio de Janeiro.
|
||||
|
||||
This paper is a personal reflection, summarising what I learned in the
|
||||
course of writing the textbook. Some of it reiterates advice that is
|
||||
well-known to some members of the dependently-typed programming
|
||||
community, but which deserves to be better known. The paper is
|
||||
organised as follows.
|
||||
|
||||
Section~2 outlines the
|
||||
topics covered in PLFA, and notes what is omitted.
|
||||
|
||||
Section~3 compares Agda and Coq as vehicles for pedagogy. Before
|
||||
writing the book, it was not obvious that it was even possible;
|
||||
conceivably, without tactics some of the proofs might
|
||||
balloon in size. In fact, it turns out that for the results in PLFA
|
||||
and SF, the proofs are of roughly comparable size, and (in my opinion)
|
||||
the proofs in PLFA are more readable and have a pleasing visual
|
||||
structure.
|
||||
|
||||
Section~4 observes that constructive proofs of progress and
|
||||
preservation combine trivially to produce a constructive evaluator for
|
||||
terms. This idea is obvious once you have seen it, yet I cannot
|
||||
find it described in the literature. For instance, SF separately
|
||||
implements a \texttt{normalise} tactic that has nothing to do with
|
||||
progress and preservation.
|
||||
|
||||
Section~5 claims that raw terms should be avoided in favour of
|
||||
inherently-typed terms. PLFA develops lambda calculus with both raw
|
||||
and inherently-typed terms, permitting a comparison. It turns out the
|
||||
former is less powerful---it supports substitution only for closed
|
||||
terms---but significantly longer---about 1.6 times as many lines of code,
|
||||
roughly the golden ratio.
|
||||
|
||||
I will argue that Agda has advantages over Coq for
|
||||
pedagogic purposes. My focus is purely on the case of a proof assistant
|
||||
as an aid to \emph{learning} formal semantics using examples of
|
||||
\emph{modest} size. I admit up front that
|
||||
there are many tasks for which Coq is better suited than Agda.
|
||||
A proof assistant that supports tactics, such as Coq or Isabelle,
|
||||
is essential for formalising serious mathematics,
|
||||
such as the Four-Colour Theorem \citep{Gonthier-2008},
|
||||
the Odd-Order Theorem \citep{Gonthier-et-al-2013},
|
||||
or Kepler's Conjecture \citep{Hales-et-al-2017},
|
||||
or for establishing correctness of software at scale,
|
||||
as with the CompCert compiler \citep{Leroy-2009,Kastner-et-al-2017}
|
||||
or the SEL4 operating system \citep{Klein-2009,O'Connor-2016}.
|
||||
|
||||
\section{Scope}
|
||||
|
||||
PLFA is aimed at students in the last year of an undergraduate
|
||||
honours programme or the first year of a master or doctorate degree.
|
||||
It aims to teach the fundamentals of operational semantics of
|
||||
programming languages, with simply-typed lambda calculus as the
|
||||
central example. The textbook is written as a literate script in Agda.
|
||||
As with SF, the hope is that using
|
||||
a proof assistant will make the development more concrete
|
||||
and accessible to students, and give them rapid feedback to find
|
||||
and correct misaprehensions.
|
||||
|
||||
The book is broken into two parts. The first part, Logical Foundations,
|
||||
develops the needed formalisms. The second part, Programming Language
|
||||
Foundations, introduces basic methods of operational semantics.
|
||||
(SF is divided into books, the first two of which have the same names
|
||||
as the two parts of PLFA, and cover similar material.)
|
||||
|
||||
Each chapter has both a one-word name and a title, the one-word name
|
||||
being both its module name and its file name.
|
||||
|
||||
\subsection*{Part I, Logical Foundations}
|
||||
|
||||
\paragraph{Naturals: Natural numbers}
|
||||
Introduces the inductive definition of natural numbers in terms of
|
||||
zero and successor, and recursive definitions of addition,
|
||||
multiplication, and monus. Emphasis is put on how a tiny description
|
||||
can specify an infinite domain.
|
||||
|
||||
\paragraph{Induction: Proof by induction}
|
||||
Introduces induction to prove properties
|
||||
such as associativity and commutativity of addition.
|
||||
Also introduces dependent functions to express universal quantification.
|
||||
Emphasis is put on the correspondence between induction and recursion.
|
||||
|
||||
\paragraph{Relations: Inductive definitions of relations}
|
||||
Introduces inductive definitions of less than or equal on natural numbers,
|
||||
and odd and even natural numbers.
|
||||
Proves properties such as reflexivity, transitivity, and
|
||||
anti-symmetry, and that the sum of two odd numbers is even.
|
||||
Emphasis is put on proof by induction over evidence that a relation holds.
|
||||
|
||||
\paragraph{Equality: Equality and equational reasoning}
|
||||
Gives Martin L\"of's and Leibniz's definitions of equality, and proves
|
||||
them equivalent, and defines the notation for equational reasoning used
|
||||
throughout the book.
|
||||
|
||||
\paragraph{Isomorphism: Isomorphism and embedding}
|
||||
Introduces isomorphism, which plays an important role in the
|
||||
subsequent development. Also introduces dependent records, lambda
|
||||
terms, and extensionality.
|
||||
|
||||
\paragraph{Connectives: Conjunction, disjunction, and implication}
|
||||
Introduces product, sum, unit, empty, and function types, and their
|
||||
interpretations as connectives of logic under Propositions as Types.
|
||||
Emphasis is put on the analogy between these types and product, sum,
|
||||
unit, zero, and exponential on naturals; e.g., product of numbers is
|
||||
commutative and product of types is commutative up to isomorphism.
|
||||
|
||||
\paragraph{Negation: Negation, with intuitionistic and classical logic}
|
||||
Introduces logical negation as a function into the empty
|
||||
type, and explains the difference between classical and intuitionistic
|
||||
logic.
|
||||
|
||||
\paragraph{Quantifiers: Universals and existentials}
|
||||
Recaps universal quantifiers and their correspondence to dependent
|
||||
functions, and introduces existential quantifiers and their
|
||||
correspondence to dependent products.
|
||||
|
||||
\paragraph{Decidable: Booleans and decision procedures}
|
||||
Introduces booleans and decidable types, and why the latter is to be
|
||||
preferred to the former.
|
||||
|
||||
\paragraph{Lists: Lists and higher-order functions}
|
||||
Gives two different definitions of reverse and proves them equivalent.
|
||||
Introduces map and fold and their properties, including that fold left
|
||||
and right are equivalent in a monoid. Introduces predicates that hold
|
||||
for all or any member of a list, with membership as a specialisation
|
||||
of the latter.
|
||||
|
||||
\subsection*{Part II, Programming Language Foundations}
|
||||
|
||||
\paragraph{Lambda: Introduction to lambda calculus}
|
||||
Introduces lambda calculus, using a representation with named
|
||||
variables and a separate typing relation. The language used is PCF
|
||||
\citep{Plotkin-1977}, with variables, lambda abstraction, application,
|
||||
zero, successor, case over naturals, and fixpoint. Reduction is
|
||||
call-by-value and restricted to closed terms.
|
||||
|
||||
\paragraph{Properties: Progress and preservation}
|
||||
Proves key properties of simply-typed
|
||||
lambda calculus, including progress and preservation. Progress and
|
||||
preservation are combined to yield an evaluator.
|
||||
|
||||
\paragraph{DeBruijn: Inherently typed de Bruijn representation}
|
||||
Introduces de Bruijn indices and the inherently-typed representation.
|
||||
Emphasis is put on the structural similarity between a term and its
|
||||
corresponding type derivation; in particular, de Bruijn indices
|
||||
correspond to the judgment that a variable is well-typed under a given
|
||||
environment.
|
||||
|
||||
\paragraph{More: More constructs of simply-typed lambda calculus}
|
||||
Introduces product, sum, unit, and empty types as well as lists and let bindings
|
||||
are explained. Typing and reduction rules are given informally; a few
|
||||
are then give formally, and the rest are left as exercises for the reader.
|
||||
The inherently typed representation is used.
|
||||
|
||||
\paragraph{Bisimulation: Relating reduction systems}
|
||||
Shows how to translate the language with ``let'' terms
|
||||
to the language without, representing a let as an application of an abstraction,
|
||||
and shows how to relate the source and target languages with a bisimulation.
|
||||
|
||||
\paragraph{Inference: Bidirectional type inference}
|
||||
Introduces bidirectional type inference, and applies it to convert from
|
||||
a representation with named variables and a separate typing relation
|
||||
to a representation de Bruijn indices with inherent types. Bidirectional
|
||||
type inference is shown to be both sound and complete.
|
||||
|
||||
\paragraph{Untyped: Untyped calculus with full normalisation}
|
||||
As a variation on earlier themes, discusses an untyped (but inherently
|
||||
scoped) lambda calculus. Reduction is call-by-name over open terms,
|
||||
with full normalisation (including reduction under lambda terms). Emphasis
|
||||
is put on the correspondence between the structure of a term and
|
||||
evidence that it is in normal form.
|
||||
|
||||
\subsection*{Discussion}
|
||||
|
||||
PLFA and SF differ in several particulars. PLFA begins with a computationally
|
||||
complete language, PCF, while SF begins with a minimal language, simply-typed
|
||||
lambda calculus with booleans. PLFA does not include type annotations in terms,
|
||||
and uses bidirectional type inference, while SF has terms with unique types and
|
||||
uses type checking. SF also covers a simple imperative language with Hoare logic,
|
||||
and for lambda calculus covers subtyping, record types, mutable references, and normalisation
|
||||
---none of which are treated by PLFA. PLFA covers an inherently-typed de Bruijn
|
||||
representation, bidirectional type inference, bisimulation, and an
|
||||
untyped call-by-name language with full normalisation---none of which
|
||||
are treated by SF.
|
||||
|
||||
SF has a third volume, written by Andrew Appel, on Verified Functional
|
||||
Algorithms. I'm not sufficiently familiar with that volume to have a view
|
||||
on whether it would be easy or hard to cover that material in Agda.
|
||||
And SF recently added a fourth volume on random testing of Coq specifications
|
||||
using QuickChick. There is currently no tool equivalent to QuickChick
|
||||
available for Agda.
|
||||
|
||||
There is more material that would be desirable to include in PLFA
|
||||
which was not due to limits of time. In future years, PLFA may be
|
||||
extended to cover additional material, including mutable references,
|
||||
normalisation, System F, pure type systems, and denotational
|
||||
semantics. I'd especially like to include pure type systems as they
|
||||
provide the readers with a formal model close to the dependent types
|
||||
used in the book. My attempts so far to formalise pure type systems
|
||||
have proved challenging, to say the least.
|
||||
|
||||
\section{Proofs in Agda and Coq}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/plfa-progress-1.png}
|
||||
\caption{PLFA, Progress (1/2)}
|
||||
\label{fig:plfa-progress-1}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[p]
|
||||
\includegraphics[width=\textwidth]{figures/plfa-progress-2.png}
|
||||
\includegraphics[width=\textwidth]{figures/plfa-progress-3a.png}
|
||||
\caption{PLFA, Progress (2/2)}
|
||||
\label{fig:plfa-progress-2}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/sf-progress-1.png}
|
||||
\caption{SF, Progress (1/2)}
|
||||
\label{fig:sf-progress-1}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/sf-progress-2.png}
|
||||
\caption{SF, Progress (2/2)}
|
||||
\label{fig:sf-progress-2}
|
||||
\end{figure}
|
||||
|
||||
% \begin{figure}[t]
|
||||
% \includegraphics[width=\textwidth]{figures/sf-progress-3.png}
|
||||
% \caption{SF, Progress (3/3)}
|
||||
% \label{fig:sf-progress-3}
|
||||
% \end{figure}
|
||||
|
||||
The introduction listed several reasons for preferring Agda over Coq.
|
||||
But Coq tactics enable more compact proofs. Would it be possible for
|
||||
PLFA to cover the same material as SF, or would the proofs
|
||||
balloon to unmanageable size?
|
||||
|
||||
As an experiment, I first rewrote SF's development of simply-typed
|
||||
lambda calculus (SF, Chapters Stlc and StlcProp) in Agda. I was a
|
||||
newbie to Agda, and translating the entire development, sticking as
|
||||
closely as possible to the development in SF, took me about two days.
|
||||
I was pleased to discover that the proofs remained about the same
|
||||
size.
|
||||
|
||||
There was also a pleasing surprise regarding the structure of the
|
||||
proofs. While most proofs in both SF and PLFA are carried out by
|
||||
induction over the evidence that a term is well typed, in SF the
|
||||
central proof, that substitution preserves types, is carried out by
|
||||
induction on terms for a technical reason
|
||||
(the context is extended by a variable binding, and hence not
|
||||
sufficiently ``generic'' to work well with Coq's induction tactic). In
|
||||
Agda, I had no trouble formulating the same proof over evidence that
|
||||
the term is well typed, and didn't even notice SF's description of the
|
||||
issue until I was done.
|
||||
|
||||
The rest of the book was relatively easy to complete. The closest to
|
||||
an issue with proof size arose when proving that reduction is
|
||||
deterministic. There are 18 cases, one case per line. Ten of the
|
||||
cases deal with the situation where there are potentially two
|
||||
different reductions; each case is trivially shown to be
|
||||
impossible. Five of the ten cases are redundant, as they just involve
|
||||
switching the order of the arguments. I had to copy the cases
|
||||
suitably permuted. It would be preferable to reinvoke the proof on
|
||||
switched arguments, but this would not pass Agda's termination checker
|
||||
since swapping the arguments doesn't yield a recursive call on
|
||||
structurally smaller arguments. I suspect tactics could cut down the
|
||||
proof significantly. I tried to compare with SF's proof that reduction
|
||||
is deterministic, but failed to find that proof.
|
||||
|
||||
SF covers an imperative language with Hoare logic, culminating in
|
||||
code that takes an imperative programme suitably decorated with preconditions
|
||||
and postconditions and generates the necessary
|
||||
verification conditions. The conditions are then verified by a custom
|
||||
tactic, where any questions of arithmetic are resolved by the
|
||||
``omega'' tactic invoking a decision procedure. The entire
|
||||
exercise would be easy to repeat in Agda, save for the last step: I
|
||||
suspect Agda's automation would not be up to verifying the generated
|
||||
conditions, requiring tedious proofs by hand. However, I had already
|
||||
decided to omit Hoare logic in order to focus on lambda calculus.
|
||||
|
||||
To give a flavour of how the texts compare, I show the
|
||||
proof of progress for simply-typed lambda calculus from both texts.
|
||||
Figures~\ref{fig:plfa-progress-1} and \ref{fig:plfa-progress-2}
|
||||
are taken from PLFA, Chapter Properties,
|
||||
while Figures~\ref{fig:sf-progress-1} and \ref{fig:sf-progress-2}
|
||||
are taken from SF, Chapter StlcProp.
|
||||
Both texts are intended to be read online,
|
||||
and the figures were taken by grabbing bitmaps of the text as
|
||||
displayed in a browser.
|
||||
|
||||
PLFA puts the formal statements first, followed by informal explanation.
|
||||
PLFA introduces an auxiliary relation \texttt{Progress} to capture
|
||||
progress; an exercise (not shown) asks the reader to show it isomorphic
|
||||
to the usual formulation with a disjunction and an existential.
|
||||
Layout is used to present the auxiliary relation in inference rule form.
|
||||
In Agda, any line beginning with two dashes is treated as a comment, making
|
||||
it easy to use a line of dashes to separate hypotheses from conclusion
|
||||
in inference rules. The proof of proposition \texttt{progress} (the different
|
||||
case making it a distinct name) is layed out carefully. The neat
|
||||
indented structure emphasises the case analysis, and all right-hand
|
||||
sides line-up in the same column. My hope as an author is that students
|
||||
will read the formal proof first, and use it as a tabular guide
|
||||
to the informal explanation that follows.
|
||||
|
||||
SF puts the informal explanation first, followed by the formal proof.
|
||||
The text hides the formal proof script under an icon;
|
||||
the figure shows what appears when the icon is expanded.
|
||||
As a teacher I was aware that
|
||||
students might skip it on a first reading, and I would have to hope the
|
||||
students would return to it and step through it with an interactive
|
||||
tool in order to make it intelligible. I expect the students skipped over
|
||||
many such proofs. This particular proof forms the basis for a question
|
||||
of the mock exam and the past exams, so I expect most students will actually
|
||||
look at this one if not all the others.
|
||||
|
||||
\newcommand{\ex}{\texttt{x}}
|
||||
\newcommand{\why}{\texttt{y}}
|
||||
\newcommand{\EL}{\texttt{L}}
|
||||
\newcommand{\EM}{\texttt{M}}
|
||||
\newcommand{\EN}{\texttt{N}}
|
||||
\newcommand{\tee}{\texttt{t}}
|
||||
\newcommand{\tick}{\texttt{\lq}}
|
||||
\newcommand{\GG}{\Gamma}
|
||||
\newcommand{\AY}{\texttt{A}}
|
||||
\newcommand{\BE}{\texttt{B}}
|
||||
|
||||
(For those wanting more detail: In PLFA, variables and abstractions and
|
||||
applications in the object language are written $\tick\;\ex$ and
|
||||
$\lambdabar\;\ex\;{\Rightarrow}\;\EN$ and $\EL\;{\cdot}\;\EM$. The
|
||||
corresponding typing rules are referred to by ${\vdash}\tick\;()$
|
||||
and ${\vdash}\lambdabar\;{\vdash}\EN$ and ${\vdash}\EL\;{\cdot}\;{\vdash}\EM$, where
|
||||
${\vdash}\EL$, ${\vdash}\EM$, ${\vdash}\EN$ are the proofs that terms
|
||||
$\EL$, $\EM$, $\EN$ are well typed, and `()` denotes that there cannot
|
||||
be evidence that a free variable is well typed in the empty context.
|
||||
It was decided to overload infix dot for readability, but not other
|
||||
symbols. In Agda, as in Lisp, almost any sequence of characters is a
|
||||
name, with spaces essential for separation.)
|
||||
|
||||
(In SF, variables and abstractions and applications in
|
||||
the object language are written $\texttt{tvar}~\ex$ and
|
||||
$\texttt{tabs}~\ex~\tee$ and $\texttt{tapp}~\tee_1~\tee_2$.
|
||||
The corresponding typing rules are referred to as
|
||||
$\texttt{T\_Var}$ and $\texttt{T\_Abs}$ and $\texttt{T\_App}$.)
|
||||
|
||||
Both Coq and Agda support interactive proof. Interaction in Coq is
|
||||
supported by Proof General, based on Emacs, or by CoqIDE, which
|
||||
provides an interactive development environment of a sort familiar to
|
||||
most students. Interaction in Agda is supported by an Emacs mode.
|
||||
|
||||
In Coq, interaction consists of stepping through a proof script, at
|
||||
each point examining the current goal and the variables currently in
|
||||
scope, and executing a new command in the script. Tactics are a whole
|
||||
sublanguage, which must be learned in addition to the language for
|
||||
expressing specifications. There are many tactics one can invoke in
|
||||
the script at each point; one menu in CoqIDE lists about one hundred
|
||||
tactics one might invoke, some in alphabetic submenus. A Coq
|
||||
script presents the specification proved and the tactics executed.
|
||||
Interaction is recorded in a script, which the students
|
||||
may step through at their leisure. SF contains some prose descriptions
|
||||
of stepping through scripts, but mainly contains scripts that students
|
||||
are encouraged to step through on their own.
|
||||
|
||||
In Agda, interaction consists of writing code with holes, at each
|
||||
point examining the current goal and the variables in scope, and
|
||||
typing code or executing an Emacs command. The number of commands
|
||||
available is much smaller than with Coq, the most important ones being
|
||||
to show the type of the hole and the types of the variables in scope;
|
||||
to check the code; to do a case analysis on a given variable; or to
|
||||
guess how to fill in the hole with constructors or variables in scope.
|
||||
An Agda proof consists of typed code. The interaction is \emph{not}
|
||||
recorded. Students may recreate it by commenting out bits of code and
|
||||
introducing a hole in their place. PLFA contains some prose descriptions
|
||||
of interactively building code, but mainly contains code that students
|
||||
can read. They may also introduce holes to interact with the code, but
|
||||
I expect this will be rarer than with SF.
|
||||
|
||||
SF encourages students to interact with all the scripts in the text.
|
||||
Trying to understand a Coq proof script without running it
|
||||
interactively is a bit like understanding a chess game by reading
|
||||
through the moves without benefit of a board, keeping it all in your
|
||||
head. In contrast, PLFA provides code that students can read.
|
||||
Understanding the code often requires working out the types, but
|
||||
(unlike executing a Coq proof script) this is often easy to do in your
|
||||
head; when it is not easy, students still have the option of
|
||||
interaction.
|
||||
|
||||
While students are keen to interact to create code, I have found they
|
||||
are reluctant to interact to understand code created by others. For
|
||||
this reason, I suspect this may make Agda a more suitable vehicle for
|
||||
teaching. Nate Foster suggests this hypothesis is ripe to be tested
|
||||
empirically, perhaps using techniques similar to those of
|
||||
\citet{Danas-et-al-2017}.
|
||||
|
||||
Neat layout of definitions such as that in
|
||||
Figure~\ref{fig:plfa-progress-2} in Emacs requires a monospaced font
|
||||
supporting all the necessary characters. Securing one has proved
|
||||
tricky. As of this writing, we use FreeMono, but it lacks a few
|
||||
characters ($\typecolon$ and $\qed$) which are loaded from fonts with a different
|
||||
width. Long arrows are necessarily more than a single character wide.
|
||||
Instead, we compose reduction —→ from an em dash — and an arrow →.
|
||||
Similarly for reflexive and transitive closure —↠.
|
||||
|
||||
\section{Progress + Preservation = Evaluation}
|
||||
|
||||
\begin{figure}
|
||||
\includegraphics[width=\textwidth]{figures/plfa-eval.png}
|
||||
\caption{PLFA, Evaluation}
|
||||
\label{fig:plfa-eval}
|
||||
\end{figure}
|
||||
|
||||
A standard approach to type soundness used by many texts,
|
||||
including SF and PLFA, is to prove progress and preservation,
|
||||
as first suggested by \citet{Wright-and-Felleisen-1994}.
|
||||
|
||||
\begin{theorem}[Progress] Given term $M$ and type $A$ such that
|
||||
$\emptyset \vdash M : A$ then either $M$ is a value or
|
||||
$M \longrightarrow N$ for some term $N$.
|
||||
\end{theorem}
|
||||
|
||||
\begin{theorem}[Preservation] Given terms $M$ and $N$ and type $A$
|
||||
such that $\emptyset \vdash M : A$ and $M \longrightarrow N$, then
|
||||
$\emptyset \vdash N : A$. \end{theorem}
|
||||
|
||||
A consequence is that when a term reduces to a value it retains
|
||||
the same type. Further, well-typed terms don't get stuck:
|
||||
that is, unable to reduce further but not yet reduced to a value.
|
||||
The formulation neatly accommodates the case of non-terminating
|
||||
reductions that never reach a value.
|
||||
|
||||
One useful by-product of the formal specification of a programming
|
||||
language may be a prototype implementation of that language. For
|
||||
instance, given a language specified by a reduction relation, such
|
||||
as lambda calculus, the prototype might accept a term and apply reductions
|
||||
to reduce it to a value. Typically, one might go to some extra work to
|
||||
create such a prototype. For instance, SF introduces a \texttt{normalize}
|
||||
tactic for this purpose. Some formal methods frameworks, such as
|
||||
Redex \citep{Felleisen-et-al-2009} and K \citep{Rosu-Serbanuta-2010},
|
||||
advertise as one of their advantages that they can generate
|
||||
a prototype from descriptions of the reduction rules.
|
||||
|
||||
I was therefore surprised to realise that any constructive proof of
|
||||
progress and preservation \emph{automatically} gives rise to such a
|
||||
prototype. The input is a term together with evidence the term is
|
||||
well-typed. (In the inherently-typed case, these are the same thing.)
|
||||
Progress determines whether we are done, or should take another step;
|
||||
preservation provides evidence that the new term is well-typed, so we
|
||||
may iterate. In a language with guaranteed termination, we cannot
|
||||
iterate forever, but there are a number of well-known techniques to
|
||||
address that issue; see, e.g., \citet{Bove-and-Capretta-2001},
|
||||
\citet{Capretta-2005}, or \citet{McBride-2015}.
|
||||
We use the simplest, similar to McBride's \emph{petrol-driven} (or
|
||||
\emph{step-indexed}) semantics: provide a maximum number of steps to
|
||||
execute; if that number proves insufficient, the evaluator returns the
|
||||
term it reached, and one can resume execution by providing a new
|
||||
number.
|
||||
|
||||
Such an evaluator from PLFA is shown in Figure~\ref{fig:plfa-eval},
|
||||
where (inspired by cryptocurrencies) the number of steps
|
||||
to execute is referred to as \emph{gas}. All of the example reduction
|
||||
sequences in PLFA were computed by the evaluator and then edited to
|
||||
improve readability; in addition, the text includes examples of
|
||||
running the evaluator with its unedited output.
|
||||
|
||||
It is immediately obvious that progress and preservation make it
|
||||
trivial to construct a prototype evaluator, and yet I cannot find such
|
||||
an observation in the literature nor mentioned in an introductory
|
||||
text. It does not appear in SF, nor in \citet{Harper-2016}. A plea
|
||||
to the Agda mailing list failed to turn up any prior mentions.
|
||||
The closest related observation I have seen in the published
|
||||
literature is that evaluators can be extracted from proofs of
|
||||
normalisation \citep{Berger-1993,Dagand-and-Scherer-2015}.
|
||||
|
||||
(Late addition: My plea to the Agda list eventually bore fruit. Oleg
|
||||
Kiselyov directed me to unpublished remarks on his web page where he
|
||||
uses the name \texttt{eval} for a proof of progress and notes ``the
|
||||
very proof of type soundness can be used to evaluate sample
|
||||
expressions'' \citep{Kiselyov-2009}.)
|
||||
|
||||
|
||||
\section{Inherent typing is golden}
|
||||
|
||||
\begin{figure}[p]
|
||||
\includegraphics[width=\textwidth]{figures/raw.png}
|
||||
\caption{Raw approach in PLFA}
|
||||
\label{fig:raw}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/inherent.png}
|
||||
\caption{Inherent approach in PLFA}
|
||||
\label{fig:inherent}
|
||||
\end{figure}
|
||||
|
||||
The second part of PLFA first discusses two different approaches to
|
||||
modelling simply-typed lambda calculus. It first presents raw
|
||||
terms with named variables and a separate typing relation and
|
||||
then shifts to inherently-typed terms with de Bruijn indices.
|
||||
Before writing the text, I had thought the two approaches
|
||||
complementary, with no clear winner. Now I am convinced that the
|
||||
inherently-typed approach is superior.
|
||||
|
||||
Figure~\ref{fig:raw} presents the raw approach.
|
||||
It first defines $\texttt{Id}$, $\texttt{Term}$,
|
||||
$\texttt{Type}$, and $\texttt{Context}$, the abstract syntax
|
||||
of identifiers, raw terms, types, and contexts.
|
||||
It then defines two judgements,
|
||||
$\GG\:{\ni}\:\ex\:{\typecolon}\:\AY$ and
|
||||
$\GG\:{\vdash}\:\EM\:{\typecolon}\:\AY$,
|
||||
which hold when under context $\GG$ the variable $\ex$
|
||||
and the term $\EM$ have type $\AY$, respectively.
|
||||
|
||||
Figure~\ref{fig:inherent} presents the inherent approach.
|
||||
It first defines $\texttt{Type}$ and $\texttt{Context}$, the abstract syntax
|
||||
of types and contexts, of which the first is as before and the second is
|
||||
as before with identifiers dropped. In place of the two judgements,
|
||||
the types of variables and terms are indexed by a context and a type,
|
||||
so that $\GG\:{\ni}\:\AY$ and $\GG\:{\vdash}\:\AY$ denote
|
||||
variables and terms, respectively, that under context $\GG$ hae type $\AY$.
|
||||
The indexed types closely resemble the previous judgements:
|
||||
we now represent a variable or a term by the proof that it is well-typed.
|
||||
In particular, the proof that a variable is well-typed in the raw approach
|
||||
corresponds to a de Bruijn index in the inherent approach.
|
||||
|
||||
The raw approach requires more lines of code than
|
||||
the inherent approach. The separate definition of raw
|
||||
terms is not needed in the inherent
|
||||
approach; and one judgement in the raw approach needs to check that
|
||||
$\ex \not\equiv \why$, while the corresponding judgement in the
|
||||
inherent approach does not. The difference becomes more pronounced
|
||||
when including the code for substitution, reductions, and proofs of
|
||||
progress and preservation. In particular, where the raw approach
|
||||
requires one first define substitution and reduction and then prove
|
||||
they preserve types, the inherent approach establishes substitution at
|
||||
the same time it defines substitution and reduction.
|
||||
|
||||
Stripping
|
||||
out examples and any proofs that appear in one but not the other (but
|
||||
could have appeared in both), the full development in PLFA for the raw approach takes 451
|
||||
lines (216 lines of definitions and 235 lines for the proofs) and the
|
||||
development for the inherent approach takes 275 lines (with
|
||||
definitions and proofs interleaved). We have 451 / 235 = 1.64,
|
||||
close to the golden ratio.
|
||||
|
||||
The inherent approach also has more expressive power. The raw
|
||||
approach is restricted to substitution of one variable by a closed
|
||||
term, while the inherent approach supports simultaneous substitution
|
||||
of all variables by open terms, using a pleasing formulation due to
|
||||
\citet{McBride-2005}, inspired by \citet{Goguen-and-McKinna-1997} and
|
||||
\citet{Altenkirch-and-Reus-1999} and described in
|
||||
\citet{Allais-et-al-2017}. In fact, I did manage to write a variant of
|
||||
the raw approach with simultaneous open substitution along the lines
|
||||
of McBride, but the result was too complex for use in an introductory
|
||||
text, requiring 695 lines of code---more than the total for the other
|
||||
two approaches combined.
|
||||
|
||||
The text develops both approaches because the raw approach is more
|
||||
familiar, and because placing the inherent approach first would
|
||||
lead to a steep learning curve. By presenting the more long-winded
|
||||
but less powerful approach first, students can see for themselves the
|
||||
advantages of de Bruijn indices and inherent types.
|
||||
|
||||
There are actually four possible designs, as the choice of named
|
||||
variables vs de Bruijn indices, and the choice of raw vs
|
||||
inherently-typed terms may be made independently. There are synergies
|
||||
beween the two. Manipulation of de Bruijn indices can be notoriously
|
||||
error-prone without inherent-typing to give assurance of correctness.
|
||||
In inherent typing with named variables, simultaneous substitution by
|
||||
open terms remains difficult.
|
||||
|
||||
The benefits of the inherent approach
|
||||
are well known to some. The technique was introduced by
|
||||
\citet{Altenkirch-and-Reus-1999}, and widely used elsewhere,
|
||||
notably by \citet{Chapman-2009} and \citet{Allais-et-al-2017}.
|
||||
I'm grateful to David Darais for bringing it to my attention.
|
||||
|
||||
|
||||
\section{Conclusion}
|
||||
|
||||
I look forward to experience teaching from the new text,
|
||||
and encourage others to use it too. Please comment!
|
||||
|
||||
|
||||
\paragraph{Acknowledgements}
|
||||
|
||||
A special thank you to my coauthor, Wen Kokke. For inventing ideas on
|
||||
which PLFA is based, and for hand-holding, many thanks to Conor
|
||||
McBride, James McKinna, Ulf Norell, and Andreas Abel. For showing me
|
||||
how much more compact it is to avoid raw terms, thanks to David
|
||||
Darais. For inspiring my work by writing SF, thanks to Benjamin
|
||||
Pierce and his coauthors. For comments on a draft of this paper, an
|
||||
extra thank you to James McKinna, Ulf Norell, Andreas Abel, and
|
||||
Benjamin Pierce. This research was supported by EPSRC Programme Grant
|
||||
EP/K034413/1.
|
||||
|
||||
|
||||
\bibliographystyle{plainnat}
|
||||
%\bibliographystyle{splncsnat.bst}
|
||||
\bibliography{PLFA}
|
||||
|
||||
|
||||
|
||||
\end{document}
|
||||
|
||||
|
||||
23
papers/scp/README.txt
Normal file
23
papers/scp/README.txt
Normal file
|
|
@ -0,0 +1,23 @@
|
|||
Look at the following when revising the paper.
|
||||
|
||||
On 2018-07-07 00:45, Philip Wadler wrote:
|
||||
Indeed, I considered using Delay for the evaluator in the textbook,
|
||||
but decided that supplying a step count was simpler, and avoided the
|
||||
need to explain coinduction.
|
||||
|
||||
In "Operational Semantics Using the Partiality Monad"
|
||||
(https://doi.org/10.1145/2364527.2364546) I defined the semantics of an
|
||||
untyped language by giving a definitional interpreter, using the delay
|
||||
monad. Then I proved type soundness for this language as a negative
|
||||
statement (using a more positive lemma):
|
||||
|
||||
[] ⊢ t ∈ σ → ¬ (⟦ t ⟧ [] ≈ fail)
|
||||
|
||||
Thus, instead of starting with type soundness and deriving an evaluator,
|
||||
I started with an evaluator and proved type soundness.
|
||||
|
||||
This kind of exercise has also been performed using fuel, see Siek's
|
||||
"Type Safety in Three Easy Lemmas"
|
||||
(http://siek.blogspot.com/2013/05/type-safety-in-three-easy-lemmas.html)
|
||||
and "Functional Big-Step Semantics" by Owens et al.
|
||||
(https://doi.org/10.1007/978-3-662-49498-1_23).
|
||||
691
papers/scp/agda.sty
Normal file
691
papers/scp/agda.sty
Normal file
|
|
@ -0,0 +1,691 @@
|
|||
% ----------------------------------------------------------------------
|
||||
% Some useful commands when doing highlighting of Agda code in LaTeX.
|
||||
% ----------------------------------------------------------------------
|
||||
|
||||
\ProvidesPackage{agda}
|
||||
|
||||
\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,
|
||||
calc, environ}
|
||||
|
||||
% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation
|
||||
\newif\ifxetexorluatex
|
||||
\ifxetex
|
||||
\xetexorluatextrue
|
||||
\else
|
||||
\ifluatex
|
||||
\xetexorluatextrue
|
||||
\else
|
||||
\xetexorluatexfalse
|
||||
\fi
|
||||
\fi
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Options
|
||||
|
||||
\DeclareOption{bw} {\newcommand{\AgdaColourScheme}{bw}}
|
||||
\DeclareOption{conor}{\newcommand{\AgdaColourScheme}{conor}}
|
||||
|
||||
\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse
|
||||
\DeclareOption{references}{
|
||||
\@AgdaEnableReferencestrue
|
||||
}
|
||||
|
||||
\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse
|
||||
\DeclareOption{links}{
|
||||
\@AgdaEnableLinkstrue
|
||||
}
|
||||
|
||||
% If the "nofontsetup" option is used, then the package does not
|
||||
% select any fonts, and it does not change the font encoding.
|
||||
\newif\if@AgdaSetupFonts\@AgdaSetupFontstrue
|
||||
\DeclareOption{nofontsetup}{
|
||||
\@AgdaSetupFontsfalse
|
||||
}
|
||||
|
||||
% If the "noinputencodingsetup" option is used, then the package does
|
||||
% not change the input encoding, and it does not load the `ucs`
|
||||
% package.
|
||||
\newif\if@AgdaSetupInputEncoding\@AgdaSetupInputEncodingtrue
|
||||
\DeclareOption{noinputencodingsetup}{
|
||||
\@AgdaSetupInputEncodingfalse
|
||||
}
|
||||
|
||||
\ProcessOptions\relax
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Input encoding setup
|
||||
|
||||
\if@AgdaSetupInputEncoding
|
||||
\ifxetexorluatex
|
||||
|
||||
\providecommand{\DeclareUnicodeCharacter}[2]{\relax}
|
||||
|
||||
\else
|
||||
|
||||
\RequirePackage{ucs}
|
||||
\RequirePackage[utf8x]{inputenc}
|
||||
|
||||
\fi
|
||||
\fi
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Font setup
|
||||
|
||||
\tracinglostchars=2 % If the font is missing some symbol, then say
|
||||
% so in the compilation output.
|
||||
|
||||
\if@AgdaSetupFonts
|
||||
% XeLaTeX or LuaLaTeX
|
||||
\ifxetexorluatex
|
||||
|
||||
% Hack to get the amsthm package working.
|
||||
% https://tex.stackexchange.com/questions/130491/xelatex-error-paragraph-ended-before-tempa-was-complete
|
||||
\let\AgdaOpenBracket\[\let\AgdaCloseBracket\]
|
||||
\RequirePackage{fontspec}
|
||||
\let\[\AgdaOpenBracket\let\]\AgdaCloseBracket
|
||||
\RequirePackage{unicode-math}
|
||||
|
||||
\setmainfont
|
||||
[ Ligatures = TeX
|
||||
, BoldItalicFont = xits-bolditalic.otf
|
||||
, BoldFont = xits-bold.otf
|
||||
, ItalicFont = xits-italic.otf
|
||||
]
|
||||
{xits-regular.otf}
|
||||
|
||||
\setmathfont{xits-math.otf}
|
||||
\setmonofont[Mapping=tex-text]{FreeMono.otf}
|
||||
|
||||
% Make mathcal and mathscr appear as different.
|
||||
% https://tex.stackexchange.com/questions/120065/xetex-what-happened-to-mathcal-and-mathscr
|
||||
\setmathfont[range={\mathcal,\mathbfcal},StylisticSet=1]{xits-math.otf}
|
||||
\setmathfont[range=\mathscr]{xits-math.otf}
|
||||
|
||||
% pdfLaTeX
|
||||
\else
|
||||
|
||||
% https://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex
|
||||
\RequirePackage[T1]{fontenc}
|
||||
|
||||
\RequirePackage{amsfonts, amssymb}
|
||||
\RequirePackage[safe]{tipa} % See page 12 of the tipa manual for what
|
||||
% safe does.
|
||||
|
||||
\fi
|
||||
\fi
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Colour schemes.
|
||||
|
||||
\providecommand{\AgdaColourScheme}{standard}
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% References to code (needs additional post-processing of tex files to
|
||||
% work, see wiki for details).
|
||||
|
||||
\if@AgdaEnableReferences
|
||||
\RequirePackage{catchfilebetweentags, xstring}
|
||||
\newcommand{\AgdaRef}[2][]{%
|
||||
\StrSubstitute{#2}{\_}{AgdaUnderscore}[\tmp]%
|
||||
\ifthenelse{\isempty{#1}}%
|
||||
{\ExecuteMetaData{AgdaTag-\tmp}}%
|
||||
{\ExecuteMetaData{#1}{AgdaTag-\tmp}}
|
||||
}
|
||||
\fi
|
||||
|
||||
\providecommand{\AgdaRef}[2][]{#2}
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Links (only done if the option is passed and the user has loaded the
|
||||
% hyperref package).
|
||||
|
||||
\if@AgdaEnableLinks
|
||||
\@ifpackageloaded{hyperref}{
|
||||
|
||||
% List that holds added targets.
|
||||
\newcommand{\AgdaList}[0]{}
|
||||
|
||||
\newtoggle{AgdaIsElem}
|
||||
\newcounter{AgdaIndex}
|
||||
\newcommand{\AgdaLookup}[3]{%
|
||||
\togglefalse{AgdaIsElem}%
|
||||
\setcounter{AgdaIndex}{0}%
|
||||
\renewcommand*{\do}[1]{%
|
||||
\ifstrequal{#1}{##1}%
|
||||
{\toggletrue{AgdaIsElem}\listbreak}%
|
||||
{\stepcounter{AgdaIndex}}}%
|
||||
\dolistloop{\AgdaList}%
|
||||
\iftoggle{AgdaIsElem}{#2}{#3}%
|
||||
}
|
||||
|
||||
\newcommand*{\AgdaTargetHelper}[1]{%
|
||||
\AgdaLookup{#1}%
|
||||
{\PackageError{agda}{``#1'' used as target more than once}%
|
||||
{Overloaded identifiers and links do not%
|
||||
work well, consider using unique%
|
||||
\MessageBreak identifiers instead.}%
|
||||
}%
|
||||
{\listadd{\AgdaList}{#1}%
|
||||
\hypertarget{Agda\theAgdaIndex}{}%
|
||||
}%
|
||||
}
|
||||
|
||||
\newcommand{\AgdaTarget}[1]{\forcsvlist{\AgdaTargetHelper}{#1}}
|
||||
|
||||
\newcommand{\AgdaLink}[1]{%
|
||||
\AgdaLookup{#1}%
|
||||
{\hyperlink{Agda\theAgdaIndex}{#1}}%
|
||||
{#1}%
|
||||
}
|
||||
}{\PackageError{agda}{Load the hyperref package before the agda package}{}}
|
||||
\fi
|
||||
|
||||
\providecommand{\AgdaTarget}[1]{}
|
||||
\providecommand{\AgdaLink}[1]{#1}
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Font styles.
|
||||
|
||||
\ifxetexorluatex
|
||||
\newcommand{\AgdaFontStyle}[1]{\ensuremath{\mathsf{#1}}}
|
||||
\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
|
||||
\newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
|
||||
}{
|
||||
\newcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathsf{#1}}}
|
||||
}
|
||||
\newcommand{\AgdaStringFontStyle}[1]{\ensuremath{\texttt{#1}}}
|
||||
\newcommand{\AgdaCommentFontStyle}[1]{\ensuremath{\texttt{#1}}}
|
||||
\newcommand{\AgdaBoundFontStyle}[1]{\ensuremath{\mathit{#1}}}
|
||||
|
||||
\else
|
||||
\newcommand{\AgdaFontStyle}[1]{\textsf{#1}}
|
||||
\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
|
||||
\newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
|
||||
}{
|
||||
\newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}}
|
||||
}
|
||||
\newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}}
|
||||
\newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}}
|
||||
\newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}}
|
||||
\fi
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Colours.
|
||||
|
||||
% ----------------------------------
|
||||
% The black and white colour scheme.
|
||||
\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
|
||||
|
||||
% Aspect colours.
|
||||
\definecolor{AgdaComment} {HTML}{000000}
|
||||
\definecolor{AgdaOption} {HTML}{000000}
|
||||
\definecolor{AgdaKeyword} {HTML}{000000}
|
||||
\definecolor{AgdaString} {HTML}{000000}
|
||||
\definecolor{AgdaNumber} {HTML}{000000}
|
||||
\definecolor{AgdaSymbol} {HTML}{000000}
|
||||
\definecolor{AgdaPrimitiveType}{HTML}{000000}
|
||||
|
||||
% NameKind colours.
|
||||
\definecolor{AgdaBound} {HTML}{000000}
|
||||
\definecolor{AgdaInductiveConstructor} {HTML}{000000}
|
||||
\definecolor{AgdaCoinductiveConstructor}{HTML}{000000}
|
||||
\definecolor{AgdaDatatype} {HTML}{000000}
|
||||
\definecolor{AgdaField} {HTML}{000000}
|
||||
\definecolor{AgdaFunction} {HTML}{000000}
|
||||
\definecolor{AgdaMacro} {HTML}{000000}
|
||||
\definecolor{AgdaModule} {HTML}{000000}
|
||||
\definecolor{AgdaPostulate} {HTML}{000000}
|
||||
\definecolor{AgdaPrimitive} {HTML}{000000}
|
||||
\definecolor{AgdaRecord} {HTML}{000000}
|
||||
\definecolor{AgdaArgument} {HTML}{000000}
|
||||
|
||||
% Other aspect colours.
|
||||
\definecolor{AgdaDottedPattern} {HTML}{000000}
|
||||
\definecolor{AgdaUnsolvedMeta} {HTML}{D3D3D3}
|
||||
\definecolor{AgdaTerminationProblem}{HTML}{BEBEBE}
|
||||
\definecolor{AgdaIncompletePattern} {HTML}{D3D3D3}
|
||||
\definecolor{AgdaError} {HTML}{696969}
|
||||
|
||||
% Misc.
|
||||
\definecolor{AgdaHole} {HTML}{BEBEBE}
|
||||
|
||||
% ----------------------------------
|
||||
% Conor McBride's colour scheme.
|
||||
}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{
|
||||
|
||||
% Aspect colours.
|
||||
\definecolor{AgdaComment} {HTML}{B22222}
|
||||
\definecolor{AgdaOption} {HTML}{000000}
|
||||
\definecolor{AgdaKeyword} {HTML}{000000}
|
||||
\definecolor{AgdaString} {HTML}{000000}
|
||||
\definecolor{AgdaNumber} {HTML}{000000}
|
||||
\definecolor{AgdaSymbol} {HTML}{000000}
|
||||
\definecolor{AgdaPrimitiveType}{HTML}{0000CD}
|
||||
|
||||
% NameKind colours.
|
||||
\definecolor{AgdaBound} {HTML}{A020F0}
|
||||
\definecolor{AgdaInductiveConstructor} {HTML}{8B0000}
|
||||
\definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000}
|
||||
\definecolor{AgdaDatatype} {HTML}{0000CD}
|
||||
\definecolor{AgdaField} {HTML}{8B0000}
|
||||
\definecolor{AgdaFunction} {HTML}{006400}
|
||||
\definecolor{AgdaMacro} {HTML}{006400}
|
||||
\definecolor{AgdaModule} {HTML}{006400}
|
||||
\definecolor{AgdaPostulate} {HTML}{006400}
|
||||
\definecolor{AgdaPrimitive} {HTML}{006400}
|
||||
\definecolor{AgdaRecord} {HTML}{0000CD}
|
||||
\definecolor{AgdaArgument} {HTML}{404040}
|
||||
|
||||
% Other aspect colours.
|
||||
\definecolor{AgdaDottedPattern} {HTML}{000000}
|
||||
\definecolor{AgdaUnsolvedMeta} {HTML}{FFD700}
|
||||
\definecolor{AgdaTerminationProblem}{HTML}{FF0000}
|
||||
\definecolor{AgdaIncompletePattern} {HTML}{A020F0}
|
||||
\definecolor{AgdaError} {HTML}{F4A460}
|
||||
|
||||
% Misc.
|
||||
\definecolor{AgdaHole} {HTML}{9DFF9D}
|
||||
|
||||
% ----------------------------------
|
||||
% The standard colour scheme.
|
||||
}{
|
||||
% Aspect colours.
|
||||
\definecolor{AgdaComment} {HTML}{B22222}
|
||||
\definecolor{AgdaOption} {HTML}{000000}
|
||||
\definecolor{AgdaKeyword} {HTML}{CD6600}
|
||||
\definecolor{AgdaString} {HTML}{B22222}
|
||||
\definecolor{AgdaNumber} {HTML}{A020F0}
|
||||
\definecolor{AgdaSymbol} {HTML}{404040}
|
||||
\definecolor{AgdaPrimitiveType}{HTML}{0000CD}
|
||||
|
||||
% NameKind colours.
|
||||
\definecolor{AgdaBound} {HTML}{000000}
|
||||
\definecolor{AgdaInductiveConstructor} {HTML}{008B00}
|
||||
\definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500}
|
||||
\definecolor{AgdaDatatype} {HTML}{0000CD}
|
||||
\definecolor{AgdaField} {HTML}{EE1289}
|
||||
\definecolor{AgdaFunction} {HTML}{0000CD}
|
||||
\definecolor{AgdaMacro} {HTML}{458B74}
|
||||
\definecolor{AgdaModule} {HTML}{A020F0}
|
||||
\definecolor{AgdaPostulate} {HTML}{0000CD}
|
||||
\definecolor{AgdaPrimitive} {HTML}{0000CD}
|
||||
\definecolor{AgdaRecord} {HTML}{0000CD}
|
||||
\definecolor{AgdaArgument} {HTML}{404040}
|
||||
|
||||
% Other aspect colours.
|
||||
\definecolor{AgdaDottedPattern} {HTML}{000000}
|
||||
\definecolor{AgdaUnsolvedMeta} {HTML}{FFFF00}
|
||||
\definecolor{AgdaTerminationProblem}{HTML}{FFA07A}
|
||||
\definecolor{AgdaIncompletePattern} {HTML}{F5DEB3}
|
||||
\definecolor{AgdaError} {HTML}{FF0000}
|
||||
|
||||
% Misc.
|
||||
\definecolor{AgdaHole} {HTML}{9DFF9D}
|
||||
}}
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Commands.
|
||||
|
||||
\newcommand{\AgdaNoSpaceMath}[1]
|
||||
{\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup}
|
||||
|
||||
% Aspect commands.
|
||||
\newcommand{\AgdaComment} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}}}
|
||||
\newcommand{\AgdaOption} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaOption}{#1}}}}
|
||||
\newcommand{\AgdaKeyword} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}}}
|
||||
\newcommand{\AgdaString} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}}}
|
||||
\newcommand{\AgdaNumber} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaNumber}{#1}}}}
|
||||
\newcommand{\AgdaSymbol} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaSymbol}{#1}}}}
|
||||
\newcommand{\AgdaPrimitiveType}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}}
|
||||
% Note that, in code generated by the LaTeX backend, \AgdaOperator is
|
||||
% always applied to a NameKind command.
|
||||
\newcommand{\AgdaOperator} [1]{#1}
|
||||
|
||||
% NameKind commands.
|
||||
|
||||
% The user can control the typesetting of (certain) individual tokens
|
||||
% by redefining the following command. The first argument is the token
|
||||
% and the second argument the thing to be typeset (sometimes just the
|
||||
% token, sometimes \AgdaLink{<the token>}). Example:
|
||||
%
|
||||
% \usepackage{ifthen}
|
||||
%
|
||||
% % Insert extra space before some tokens.
|
||||
% \DeclareRobustCommand{\AgdaFormat}[2]{%
|
||||
% \ifthenelse{
|
||||
% \equal{#1}{≡⟨} \OR
|
||||
% \equal{#1}{≡⟨⟩} \OR
|
||||
% \equal{#1}{∎}
|
||||
% }{\ }{}#2}
|
||||
%
|
||||
% Note the use of \DeclareRobustCommand.
|
||||
|
||||
\newcommand{\AgdaFormat}[2]{#2}
|
||||
|
||||
\newcommand{\AgdaBound}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaBound}{\AgdaFormat{#1}{#1}}}}}
|
||||
\newcommand{\AgdaInductiveConstructor}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaCoinductiveConstructor}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaDatatype}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaDatatype}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaField}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaField}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaFunction}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaFunction}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaMacro}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaMacro}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaModule}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaModule}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaPostulate}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPostulate}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaPrimitive}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitive}{\AgdaFormat{#1}{#1}}}}}
|
||||
\newcommand{\AgdaRecord}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaRecord}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaArgument}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaArgument}{\AgdaFormat{#1}{#1}}}}}
|
||||
|
||||
% Other aspect commands.
|
||||
\newcommand{\AgdaFixityOp} [1]{\AgdaNoSpaceMath{$#1$}}
|
||||
\newcommand{\AgdaDottedPattern} [1]{\textcolor{AgdaDottedPattern}{#1}}
|
||||
\newcommand{\AgdaUnsolvedMeta} [1]
|
||||
{\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}}
|
||||
\newcommand{\AgdaTerminationProblem}[1]
|
||||
{\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}}
|
||||
\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}}
|
||||
\newcommand{\AgdaError} [1]
|
||||
{\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}}
|
||||
\newcommand{\AgdaCatchallClause} [1]{#1} % feel free to change this
|
||||
|
||||
% Used to hide code from LaTeX.
|
||||
%
|
||||
% Note that this macro has been deprecated in favour of giving the
|
||||
% hide argument to the code environment.
|
||||
\long\def\AgdaHide#1{\ignorespaces}
|
||||
|
||||
% Misc.
|
||||
\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% The code environment.
|
||||
|
||||
\newcommand{\AgdaCodeStyle}{}
|
||||
% \newcommand{\AgdaCodeStyle}{\tiny}
|
||||
|
||||
\ifdefined\mathindent
|
||||
{}
|
||||
\else
|
||||
\newdimen\mathindent\mathindent\leftmargini
|
||||
\fi
|
||||
|
||||
% Adds the given amount of vertical space and starts a new line.
|
||||
%
|
||||
% The implementation comes from lhs2TeX's polycode.fmt, written by
|
||||
% Andres Löh.
|
||||
\newcommand{\Agda@NewlineWithVerticalSpace}[1]{%
|
||||
{\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}
|
||||
|
||||
% Should there be space around code?
|
||||
\newboolean{Agda@SpaceAroundCode}
|
||||
|
||||
% Use this command to avoid extra space around code blocks.
|
||||
\newcommand{\AgdaNoSpaceAroundCode}{%
|
||||
\setboolean{Agda@SpaceAroundCode}{false}}
|
||||
|
||||
% Use this command to include extra space around code blocks.
|
||||
\newcommand{\AgdaSpaceAroundCode}{%
|
||||
\setboolean{Agda@SpaceAroundCode}{true}}
|
||||
|
||||
% By default space is inserted around code blocks.
|
||||
\AgdaSpaceAroundCode{}
|
||||
|
||||
% Sometimes one might want to break up a code block into multiple
|
||||
% pieces, but keep code in different blocks aligned with respect to
|
||||
% each other. Then one can use the AgdaAlign environment. Example
|
||||
% usage:
|
||||
%
|
||||
% \begin{AgdaAlign}
|
||||
% \begin{code}
|
||||
% code
|
||||
% code (more code)
|
||||
% \end{code}
|
||||
% Explanation...
|
||||
% \begin{code}
|
||||
% aligned with "code"
|
||||
% code (aligned with (more code))
|
||||
% \end{code}
|
||||
% \end{AgdaAlign}
|
||||
%
|
||||
% Note that AgdaAlign environments should not be nested.
|
||||
%
|
||||
% Sometimes one might also want to hide code in the middle of a code
|
||||
% block. This can be accomplished in the following way:
|
||||
%
|
||||
% \begin{AgdaAlign}
|
||||
% \begin{code}
|
||||
% visible
|
||||
% \end{code}
|
||||
% \begin{code}[hide]
|
||||
% hidden
|
||||
% \end{code}
|
||||
% \begin{code}
|
||||
% visible
|
||||
% \end{code}
|
||||
% \end{AgdaAlign}
|
||||
%
|
||||
% However, the result may be ugly: extra space is perhaps inserted
|
||||
% around the code blocks.
|
||||
%
|
||||
% The AgdaSuppressSpace environment ensures that extra space is only
|
||||
% inserted before the first code block, and after the last one (but
|
||||
% not if \AgdaNoSpaceAroundCode{} is used). Example usage:
|
||||
%
|
||||
% \begin{AgdaAlign}
|
||||
% \begin{code}
|
||||
% code
|
||||
% more code
|
||||
% \end{code}
|
||||
% Explanation...
|
||||
% \begin{AgdaSuppressSpace}
|
||||
% \begin{code}
|
||||
% aligned with "code"
|
||||
% aligned with "more code"
|
||||
% \end{code}
|
||||
% \begin{code}[hide]
|
||||
% hidden code
|
||||
% \end{code}
|
||||
% \begin{code}
|
||||
% also aligned with "more code"
|
||||
% \end{code}
|
||||
% \end{AgdaSuppressSpace}
|
||||
% \end{AgdaAlign}
|
||||
%
|
||||
% Note that AgdaSuppressSpace environments should not be nested.
|
||||
%
|
||||
% There is also a combined environment, AgdaMultiCode, that combines
|
||||
% the effects of AgdaAlign and AgdaSuppressSpace.
|
||||
|
||||
% The number of the current/next code block (excluding hidden ones).
|
||||
\newcounter{Agda@Current}
|
||||
\setcounter{Agda@Current}{0}
|
||||
|
||||
% The number of the previous code block (excluding hidden ones), used
|
||||
% locally in \Agda@SuppressEnd.
|
||||
\newcounter{Agda@Previous}
|
||||
|
||||
% Is AgdaAlign active?
|
||||
\newboolean{Agda@Align}
|
||||
\setboolean{Agda@Align}{false}
|
||||
|
||||
% The number of the first code block (if any) in a given AgdaAlign
|
||||
% environment.
|
||||
\newcounter{Agda@AlignStart}
|
||||
|
||||
\newcommand{\Agda@AlignStart}{%
|
||||
\ifthenelse{\boolean{Agda@Align}}{%
|
||||
\PackageError{agda}{Nested AgdaAlign environments}{%
|
||||
AgdaAlign and AgdaMultiCode environments must not be
|
||||
nested.}}{%
|
||||
\setboolean{Agda@Align}{true}%
|
||||
\setcounter{Agda@AlignStart}{\value{Agda@Current}}}}
|
||||
|
||||
\newcommand{\Agda@AlignEnd}{\setboolean{Agda@Align}{false}}
|
||||
|
||||
\newenvironment{AgdaAlign}{%
|
||||
\Agda@AlignStart{}}{%
|
||||
\Agda@AlignEnd{}%
|
||||
\ignorespacesafterend}
|
||||
|
||||
% Is AgdaSuppressSpace active?
|
||||
\newboolean{Agda@Suppress}
|
||||
\setboolean{Agda@Suppress}{false}
|
||||
|
||||
% The number of the first code block (if any) in a given
|
||||
% AgdaSuppressSpace environment.
|
||||
\newcounter{Agda@SuppressStart}
|
||||
|
||||
% Does a "do not suppress space after" label exist for the current
|
||||
% code block? (This boolean is used locally in the code environment's
|
||||
% implementation.)
|
||||
\newboolean{Agda@DoNotSuppressSpaceAfter}
|
||||
|
||||
\newcommand{\Agda@SuppressStart}{%
|
||||
\ifthenelse{\boolean{Agda@Suppress}}{%
|
||||
\PackageError{agda}{Nested AgdaSuppressSpace environments}{%
|
||||
AgdaSuppressSpace and AgdaMultiCode environments must not be
|
||||
nested.}}{%
|
||||
\setboolean{Agda@Suppress}{true}%
|
||||
\setcounter{Agda@SuppressStart}{\value{Agda@Current}}}}
|
||||
|
||||
% Marks the given code block as one that space should not be
|
||||
% suppressed after (if AgdaSpaceAroundCode and AgdaSuppressSpace are
|
||||
% both active).
|
||||
\newcommand{\Agda@DoNotSuppressSpaceAfter}[1]{%
|
||||
% The use of labels is intended to ensure that LaTeX will provide a
|
||||
% warning if the document needs to be recompiled.
|
||||
\label{Agda@DoNotSuppressSpaceAfter@#1}}
|
||||
|
||||
\newcommand{\Agda@SuppressEnd}{%
|
||||
\ifthenelse{\value{Agda@SuppressStart} = \value{Agda@Current}}{}{%
|
||||
% Mark the previous code block in the .aux file.
|
||||
\setcounter{Agda@Previous}{\theAgda@Current-1}%
|
||||
\immediate\write\@auxout{%
|
||||
\noexpand\Agda@DoNotSuppressSpaceAfter{\theAgda@Previous}}}%
|
||||
\setboolean{Agda@Suppress}{false}}
|
||||
|
||||
\newenvironment{AgdaSuppressSpace}{%
|
||||
\Agda@SuppressStart{}}{%
|
||||
\Agda@SuppressEnd{}%
|
||||
\ignorespacesafterend}
|
||||
|
||||
\newenvironment{AgdaMultiCode}{%
|
||||
\Agda@AlignStart{}%
|
||||
\Agda@SuppressStart{}}{%
|
||||
\Agda@SuppressEnd{}%
|
||||
\Agda@AlignEnd{}%
|
||||
\ignorespacesafterend}
|
||||
|
||||
% Vertical space used for empty lines. By default \baselineskip.
|
||||
\newlength{\AgdaEmptySkip}
|
||||
\setlength{\AgdaEmptySkip}{\baselineskip}
|
||||
|
||||
% Extra space to be inserted for empty lines (the difference between
|
||||
% \AgdaEmptySkip and \baselineskip). Used internally.
|
||||
\newlength{\AgdaEmptyExtraSkip}
|
||||
|
||||
% The code environment.
|
||||
%
|
||||
% Code can be hidden by writing \begin{code}[hide].
|
||||
%
|
||||
% The implementation is based on plainhscode in lhs2TeX's
|
||||
% polycode.fmt, written by Andres Löh.
|
||||
\NewEnviron{code}[1][]{%
|
||||
% Conditionally hide the code.
|
||||
\ifthenelse{\equal{#1}{hide}}{}{%
|
||||
%
|
||||
% Conditionally emit space before the code block. Unconditionally
|
||||
% switch to a new line.
|
||||
\ifthenelse{\boolean{Agda@SpaceAroundCode} \and%
|
||||
\(\not \boolean{Agda@Suppress} \or%
|
||||
\value{Agda@SuppressStart} = \value{Agda@Current}\)}{%
|
||||
\Agda@NewlineWithVerticalSpace{\abovedisplayskip}}{%
|
||||
\Agda@NewlineWithVerticalSpace{0pt}}%
|
||||
%
|
||||
% Indent the entire code block.
|
||||
\advance\leftskip\mathindent%
|
||||
%
|
||||
% The code's style can be customised.
|
||||
\AgdaCodeStyle%
|
||||
%
|
||||
% Used to control the height of empty lines.
|
||||
\setlength{\AgdaEmptyExtraSkip}{\AgdaEmptySkip - \baselineskip}%
|
||||
%
|
||||
% The environment used to handle indentation (of individual lines)
|
||||
% and alignment.
|
||||
\begin{pboxed}%
|
||||
%
|
||||
% Conditionally preserve alignment between code blocks.
|
||||
\ifthenelse{\boolean{Agda@Align}}{%
|
||||
\ifthenelse{\value{Agda@AlignStart} = \value{Agda@Current}}{%
|
||||
\savecolumns}{%
|
||||
\restorecolumns}}{}%
|
||||
%
|
||||
% The code.
|
||||
\BODY%
|
||||
\end{pboxed}%
|
||||
%
|
||||
% Does the label Agda@DoNotSuppressAfter@<current code block
|
||||
% number> exist?
|
||||
\ifcsdef{r@Agda@DoNotSuppressSpaceAfter@\theAgda@Current}{%
|
||||
\setboolean{Agda@DoNotSuppressSpaceAfter}{true}}{%
|
||||
\setboolean{Agda@DoNotSuppressSpaceAfter}{false}}%
|
||||
%
|
||||
% Conditionally emit space after the code block. Unconditionally
|
||||
% switch to a new line.
|
||||
\ifthenelse{\boolean{Agda@SpaceAroundCode} \and%
|
||||
\(\not \boolean{Agda@Suppress} \or%
|
||||
\boolean{Agda@DoNotSuppressSpaceAfter}\)}{%
|
||||
\Agda@NewlineWithVerticalSpace{\belowdisplayskip}}{%
|
||||
\Agda@NewlineWithVerticalSpace{0pt}}%
|
||||
%
|
||||
% Step the code block counter, but only for non-hidden code.
|
||||
\stepcounter{Agda@Current}}}
|
||||
|
||||
% Space inserted after tokens.
|
||||
\newcommand{\AgdaSpace}{ }
|
||||
|
||||
% Space inserted to indent something.
|
||||
\newcommand{\AgdaIndentSpace}{\AgdaSpace{}$\;\;$}
|
||||
|
||||
% Default column for polytable.
|
||||
\defaultcolumn{@{}l@{\AgdaSpace{}}}
|
||||
|
||||
% \AgdaIndent expects a non-negative integer as its only argument.
|
||||
% This integer should be the distance, in code blocks, to the thing
|
||||
% relative to which the text is indented.
|
||||
%
|
||||
% The default implementation only indents if the thing that the text
|
||||
% is indented relative to exists in the same code block or is wrapped
|
||||
% in the same AgdaAlign or AgdaMultiCode environment.
|
||||
\newcommand{\AgdaIndent}[1]{%
|
||||
\ifthenelse{#1 = 0
|
||||
\or
|
||||
\( \boolean{Agda@Align}
|
||||
\and
|
||||
\cnttest{\value{Agda@Current} - #1}{>=}{
|
||||
\value{Agda@AlignStart}}
|
||||
\)}{\AgdaIndentSpace{}}{}}
|
||||
|
||||
% Underscores are typeset using \AgdaUnderscore{}.
|
||||
\newcommand{\AgdaUnderscore}{\_}
|
||||
|
||||
\endinput
|
||||
BIN
papers/scp/copyright.pdf
Normal file
BIN
papers/scp/copyright.pdf
Normal file
Binary file not shown.
32
papers/scp/extra.lagda
Normal file
32
papers/scp/extra.lagda
Normal file
|
|
@ -0,0 +1,32 @@
|
|||
\section{Code}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/InherentIndices.png}
|
||||
\caption{Indices}
|
||||
\label{fig:indices}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/InherentSubst.png}
|
||||
\caption{Substitution}
|
||||
\label{fig:subst}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/InherentReductions.png}
|
||||
\caption{Reductions}
|
||||
\label{fig:reductions}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/InherentProgress.png}
|
||||
\caption{Progress}
|
||||
\label{fig:progress}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/InherentEval.png}
|
||||
\caption{Evaluation}
|
||||
\label{fig:eval}
|
||||
\end{figure}
|
||||
|
||||
BIN
papers/scp/figures/InherentEval.png
Normal file
BIN
papers/scp/figures/InherentEval.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 168 KiB |
BIN
papers/scp/figures/InherentIndices.png
Normal file
BIN
papers/scp/figures/InherentIndices.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 105 KiB |
BIN
papers/scp/figures/InherentProgress.png
Normal file
BIN
papers/scp/figures/InherentProgress.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 120 KiB |
BIN
papers/scp/figures/InherentReductions.png
Normal file
BIN
papers/scp/figures/InherentReductions.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 148 KiB |
BIN
papers/scp/figures/InherentSubst.png
Normal file
BIN
papers/scp/figures/InherentSubst.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 208 KiB |
BIN
papers/scp/figures/InherentTerms.png
Normal file
BIN
papers/scp/figures/InherentTerms.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 135 KiB |
BIN
papers/scp/figures/inherent.png
Normal file
BIN
papers/scp/figures/inherent.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 25 KiB |
BIN
papers/scp/figures/plfa-eval.png
Normal file
BIN
papers/scp/figures/plfa-eval.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 240 KiB |
BIN
papers/scp/figures/plfa-progress-1.png
Normal file
BIN
papers/scp/figures/plfa-progress-1.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 275 KiB |
BIN
papers/scp/figures/plfa-progress-2.png
Normal file
BIN
papers/scp/figures/plfa-progress-2.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 211 KiB |
BIN
papers/scp/figures/plfa-progress-3.png
Normal file
BIN
papers/scp/figures/plfa-progress-3.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 473 KiB |
BIN
papers/scp/figures/plfa-progress-3a.png
Normal file
BIN
papers/scp/figures/plfa-progress-3a.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 360 KiB |
BIN
papers/scp/figures/plfa-progress-3b.png
Normal file
BIN
papers/scp/figures/plfa-progress-3b.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 334 KiB |
BIN
papers/scp/figures/raw.png
Normal file
BIN
papers/scp/figures/raw.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 36 KiB |
BIN
papers/scp/figures/sf-progress-1.png
Normal file
BIN
papers/scp/figures/sf-progress-1.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 379 KiB |
BIN
papers/scp/figures/sf-progress-2.png
Normal file
BIN
papers/scp/figures/sf-progress-2.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 260 KiB |
BIN
papers/scp/figures/sf-progress-3.png
Normal file
BIN
papers/scp/figures/sf-progress-3.png
Normal file
Binary file not shown.
|
After Width: | Height: | Size: 86 KiB |
BIN
papers/scp/final.zip
Normal file
BIN
papers/scp/final.zip
Normal file
Binary file not shown.
660
papers/scp/latex/PLFA.tex
Normal file
660
papers/scp/latex/PLFA.tex
Normal file
|
|
@ -0,0 +1,660 @@
|
|||
%\documentclass[runningheads,oribibl]{llncs}
|
||||
\documentclass[runningheads]{llncs}
|
||||
\usepackage{natbib}
|
||||
% \usepackage{stmaryrd}
|
||||
% \usepackage{proof}
|
||||
% \usepackage{amsmath}
|
||||
% \usepackage{amssymb}
|
||||
% \usepackage{color}
|
||||
% \usepackage{bbm}
|
||||
% \usepackage[greek,english]{babel}
|
||||
% \usepackage{ucs}
|
||||
% \usepackage[utf8x]{inputenc}
|
||||
% \usepackage{autofe}
|
||||
\usepackage{agda}
|
||||
\usepackage{graphicx}
|
||||
\usepackage{url}
|
||||
\renewcommand\UrlFont{\color{blue}\rmfamily}
|
||||
\usepackage{stix}
|
||||
\setcitestyle{round,aysep={}}
|
||||
|
||||
\DeclareUnicodeCharacter{"2982}{\ensuremath{\typecolon}} % ⦂
|
||||
\DeclareUnicodeCharacter{"220E}{\ensuremath{\QED}} % ∎
|
||||
|
||||
\begin{document}
|
||||
\title{Programming Language Foundations in Agda}
|
||||
\author{Philip Wadler}
|
||||
\authorrunning{P. Wadler}
|
||||
\institute{University of Edinburgh\\
|
||||
\email{wadler@inf.ed.ac.uk}}
|
||||
\maketitle
|
||||
%
|
||||
\begin{abstract}
|
||||
The leading textbook for formal methods is \emph{Software Foundations}
|
||||
(SF), written by Benjamin Pierce in collaboration with others, and
|
||||
based on Coq. After five years using SF in the classroom, I have come
|
||||
to the conclusion that Coq is not the best vehicle for this purpose,
|
||||
as too much of the course needs to focus on learning tactics for proof
|
||||
derivation, to the cost of learning programming language theory.
|
||||
Accordingly, I have written a new textbook, \emph{Programming Language
|
||||
Foundations in Agda} (PLFA). PLFA covers much of the same ground as
|
||||
SF, although it is not a slavish imitation.
|
||||
|
||||
What did I learn from writing PLFA? First, that it is possible. One
|
||||
might expect that without proof tactics that the proofs become too
|
||||
long, but in fact proofs in PLFA are about the same length as those in
|
||||
SF. Proofs in Coq require an interactive environment to be understood,
|
||||
while proofs in Agda can be read on the page. Second, that
|
||||
constructive proofs of preservation and progress give immediate rise
|
||||
to a prototype evaluator. This fact is obvious in retrospect but it is
|
||||
not exploited in SF (which instead provides a separate normalise
|
||||
tactic) nor can I find it in the literature. Third, that using raw
|
||||
terms with a separate typing relation is far less perspicuous than
|
||||
using inherently-typed terms. SF uses the former presentation, while
|
||||
PLFA presents both; the former uses about 1.6 as many lines of Agda
|
||||
code as the latter, roughly the golden ratio.
|
||||
|
||||
The textbook is written as a literate Agda script, and can be found here:
|
||||
\begin{center}
|
||||
\url{http://plfa.inf.ed.ac.uk}
|
||||
\end{center}
|
||||
\keywords{Agda \and Coq \and lambda calculus \and dependent types.}
|
||||
\end{abstract}
|
||||
|
||||
\section{Introduction}
|
||||
|
||||
The most profound connection between logic and computation is a pun.
|
||||
The doctrine of Propositions as Types asserts that a certain kind of formal
|
||||
structure may be read in two ways: either as a proposition in logic or
|
||||
as a type in computing. Further, a related structure may be read as
|
||||
either the proof of the proposition or as a programme of the
|
||||
corresponding type. Further still, simplification of proofs
|
||||
corresponds to evaluation of programs.
|
||||
|
||||
Accordingly, the title of this paper, and the corresponding textbook,
|
||||
\emph{Programming Language Foundations in Agda} (hence, PLFA)
|
||||
also has two readings. It may be parsed as ``(Programming Language)
|
||||
Foundations in Agda'' or ``Programming (Language Foundations) in
|
||||
Agda''---the specifications in the proof assistant Agda both describe
|
||||
programming languages and are themselves programmes.
|
||||
|
||||
Since 2013, I have taught a course on Types and Semantics for
|
||||
Programming Languages to fourth-year undergraduates and masters
|
||||
students at the University of Edinburgh. An earlier version of that
|
||||
course was based on \emph{Types and Programming Languages} by
|
||||
\citet{Pierce-2002}, but my version was taught from its successor,
|
||||
\emph{Software Foundations} (hence, SF) by \citet{Pierce-et-al-2010},
|
||||
which is based on the proof assistance Coq \citep{Huet-et-al-1997}.
|
||||
I am convinced by the claim of \citet{Pierce-2009}, made in his ICFP
|
||||
Keynote \emph{Lambda, The Ultimate TA}, that basing a course around a
|
||||
proof assistant aids learning.
|
||||
|
||||
However, after five years of experience, I have come to the conclusion
|
||||
that Coq is not the best vehicle. Too much of the course needs to
|
||||
focus on learning tactics for proof derivation, to the cost of
|
||||
learning the fundamentals of programming language theory. Every
|
||||
concept has to be learned twice: e.g., both the product data type, and
|
||||
the corresponding tactics for introduction and elimination of
|
||||
conjunctions. The rules Coq applies to generate induction hypotheses
|
||||
can sometimes seem mysterious. While the \texttt{notation} construct
|
||||
permits pleasingly flexible syntax, it can be confusing that the same
|
||||
concept must always be given two names, e.g., both
|
||||
\texttt{subst~N~x~M} and \texttt{N~[x~:=~M]}. Names of tactics are
|
||||
sometimes short and sometimes long; naming conventions in the standard
|
||||
library can be wildly inconsistent. \emph{Propositions as types} as a
|
||||
foundation of proof is present but hidden.
|
||||
|
||||
I found myself keen to recast the course in Agda \citep{Bove-et-al-2009}.
|
||||
In Agda, there is
|
||||
no longer any need to learn about tactics: there is just
|
||||
dependently-typed programming, plain and simple. Introduction is
|
||||
always by a constructor, elimination is always by pattern
|
||||
matching. Induction is no longer a mysterious separate concept, but
|
||||
corresponds to the familiar notion of recursion. Mixfix syntax is
|
||||
flexible while using just one name for each concept, e.g.,
|
||||
substitution is \texttt{\_[\_:=\_]}. The standard library is not perfect, but
|
||||
there is a fair attempt at consistency. \emph{Propositions as types} as a
|
||||
foundation of proof is on proud display.
|
||||
|
||||
Alas, there is no textbook for programming language theory in
|
||||
Agda. \emph{Verified Functional Programming in Agda} by \citep{Stump-2016}
|
||||
covers related ground, but focusses more on programming with dependent
|
||||
types than on the theory of programming languages.
|
||||
|
||||
The original goal was to simply adapt \emph{Software Foundations},
|
||||
maintaining the same text but transposing the code from Coq to Agda.
|
||||
But it quickly became clear to me that after five years in the
|
||||
classroom I had my own ideas about how to present the material. They
|
||||
say you should never write a book unless you cannot \emph{not} write the
|
||||
book, and I soon found that this was a book I could not not write.
|
||||
|
||||
I am fortunate that my student, Wen Kokke, was keen to help. She
|
||||
guided me as a newbie to Agda and provided an infrastructure that is
|
||||
easy to use and produces pages that are a pleasure to view.
|
||||
The bulk of the book was written January--June 2018, while on
|
||||
sabbatical in Rio de Janeiro.
|
||||
|
||||
This paper is a personal reflection, summarising what I learned in the
|
||||
course of writing the textbook. Some of it reiterates advice that is
|
||||
well-known to some members of the dependently-typed programming
|
||||
community, but which deserves to be better known. The paper is
|
||||
organised as follows.
|
||||
|
||||
Section~2 outlines the
|
||||
topics covered in PLFA, and notes what is omitted.
|
||||
|
||||
Section~3 compares Agda and Coq as vehicles for pedagogy. Before
|
||||
writing the book, it was not obvious that it was even possible;
|
||||
conceivably, without tactics some of the proofs
|
||||
balloon in size. In fact, it turns out that for the results in PLFA
|
||||
and SF, the proofs are of roughly comparable size, and (in my opinion)
|
||||
the proofs in PLFA are more readable and have a pleasing visual
|
||||
structure.
|
||||
|
||||
Section~4 observes that constructive proofs of progress and
|
||||
preservation combine trivially to produce a constructive evaluator for
|
||||
terms. This idea is obvious once you have seen it, yet I cannot
|
||||
find it described in the literature. For instance, SF separately
|
||||
implements a \texttt{normalise} tactic that has nothing to do with
|
||||
progress and preservation.
|
||||
|
||||
Section~5 claims that raw terms should be avoided in favour of
|
||||
inherently-typed terms. PLFA develops lambda calculus with both raw
|
||||
and inherently-typed terms, permitting a comparison. It turns out the
|
||||
former is less powerful---it supports substitution only for closed
|
||||
terms---but significantly longer---about 1.6 times as many lines of code,
|
||||
roughly the golden ratio.
|
||||
|
||||
I will argue that Agda has advantages over Coq for
|
||||
pedagogic purposes. My focus is purely on the case of a proof assistant
|
||||
as an aid to \emph{learning} formal semantics using examples of
|
||||
\emph{modest} size. I admit up front that
|
||||
there are many tasks for which Coq is better suited than Agda.
|
||||
A proof assistant that supports tactics, such as Coq or Isabelle,
|
||||
is essential for formalising serious mathematics,
|
||||
such as the Four-Colour Theorem \citep{Gonthier-2008},
|
||||
the Odd-Order Theorem \citep{Gonthier-et-al-2013},
|
||||
or Kepler's Conjecture \citep{Hales-et-al-2017},
|
||||
or for establishing correctness of software at scale,
|
||||
as with the CompCert compiler \citep{Leroy-2009,Kastner-et-al-2017}
|
||||
or the SEL4 operating system \citep{Klein-2009,O'Connor-2016}.
|
||||
|
||||
\section{Scope}
|
||||
|
||||
PLFA is aimed at students in the last year of an undergraduate
|
||||
honours programme or the first year of a master or doctorate degree.
|
||||
It aims to teach the fundamentals of operational semantics of
|
||||
programming languages, with simply-typed lambda calculus as the
|
||||
central example. The textbook is written as a literate script in Agda.
|
||||
As with SF, the hope is that using
|
||||
a proof assistant will make the development more concrete
|
||||
and accessible to students, and give them rapid feedback to find
|
||||
and correct misaprehensions.
|
||||
|
||||
The book is broken into two parts. The first part, Logical Foundations,
|
||||
develops the needed formalisms. The second part, Programming Language
|
||||
Foundations, introduces basic methods of operational semantics.
|
||||
(SF is divided into books, the first two of which have the same names
|
||||
as the two parts of PLFA, and cover similar material.)
|
||||
|
||||
Each chapter has both a one-word name and a title, the one-word name
|
||||
being both its module name and its file name.
|
||||
|
||||
\subsection*{Part I, Logical Foundations}
|
||||
|
||||
\paragraph{Naturals: Natural numbers}
|
||||
Introduces the inductive definition of natural numbers in terms of
|
||||
zero and successor, and recursive definitions of addition,
|
||||
multiplication, and monus. Emphasis is put on how a tiny description
|
||||
can specify an infinite domain.
|
||||
|
||||
\paragraph{Induction: Proof by induction}
|
||||
Introduces induction to prove properties
|
||||
such as associativity and commutativity of addition.
|
||||
Also introduces dependent functions to express universal quantification.
|
||||
Emphasis is put on the correspondence between induction and recursion.
|
||||
|
||||
\paragraph{Relations: Inductive definitions of relations}
|
||||
Introduces inductive definitions of less than or equal on natural numbers,
|
||||
and odd and even natural numbers.
|
||||
Proves properties such as reflexivity, transitivity, and
|
||||
anti-symmetry, and that the sum of two odd numbers is even.
|
||||
Emphasis is put on proof by induction over evidence that a relation holds.
|
||||
|
||||
\paragraph{Equality: Equality and equational reasoning}
|
||||
Gives Martin L\"of's and Leibniz's definitions of equality, and proves
|
||||
them equivalent, and defines the notation for equational reasoning used
|
||||
throughout the book.
|
||||
|
||||
\paragraph{Isomorphism: Isomorphism and embedding}
|
||||
Introduces isomorphism, which plays an important role in the
|
||||
subsequent development. Also introduces dependent records, lambda
|
||||
terms, and extensionality.
|
||||
|
||||
\paragraph{Connectives: Conjunction, disjunction, and implication}
|
||||
Introduces product, sum, unit, empty, and function types, and their
|
||||
interpretations as connectives of logic under Propositions as Types.
|
||||
Emphasis is put on the analogy between these types and product, sum,
|
||||
unit, zero, and exponential on naturals; e.g., product of numbers is
|
||||
commutative and product of types is commutative up to isomorphism.
|
||||
|
||||
\paragraph{Negation: Negation, with intuitionistic and classical logic}
|
||||
Introduces logical negation as a function into the empty
|
||||
type, and explains the difference between classical and intuitionistic
|
||||
logic.
|
||||
|
||||
\paragraph{Quantifiers: Universals and existentials}
|
||||
Recaps universal quantifiers and their correspondence to dependent
|
||||
functions, and introduces existential quantifiers and their
|
||||
correspondence to dependent products.
|
||||
|
||||
\paragraph{Lists: Lists and higher-order functions}
|
||||
Gives two different definitions of reverse and proves them equivalent.
|
||||
Introduces map and fold and their properties, including that fold left
|
||||
and right are equivalent in a monoid. Introduces predicates that hold
|
||||
for all or any member of a list, with membership as a specialisation
|
||||
of the latter.
|
||||
|
||||
\paragraph{Decidable: Booleans and decision procedures}
|
||||
Introduces booleans and decidable types, and why the latter is to be
|
||||
preferred to the former.
|
||||
|
||||
\subsection*{Part II, Programming Language Foundations}
|
||||
|
||||
\paragraph{Lambda: Introduction to lambda calculus}
|
||||
Introduces lambda calculus, using a representation with named
|
||||
variables and a separate typing relation. The language used is PCF,
|
||||
with variables, lambda abstraction, application, zero, successor, case
|
||||
over naturals, and fixpoint. Reduction is call-by-value and restricted
|
||||
to closed terms.
|
||||
|
||||
\paragraph{Properties: Progress and preservation}
|
||||
Proves key properties of simply-typed
|
||||
lambda calculus, including progress and preservation. Progress and
|
||||
preservation are combined to yield an evaluator.
|
||||
|
||||
\paragraph{DeBruijn: Inherently typed de Bruijn representation}
|
||||
Introduces de Bruijn numbers and the inherently-typed representation.
|
||||
Emphasis is put on the structural similarity between a term and its
|
||||
corresponding type derivation; in particular, de Bruijn numbers
|
||||
correspond to the judgment that a variable is well-typed under a given
|
||||
environment.
|
||||
|
||||
\paragraph{More: More constructs of simply-typed lambda calculus}
|
||||
Introduces product, sum, unit, and empty types as well as lists and let bindings
|
||||
are explained. Typing and reduction rules are given informally; a few
|
||||
are then give formally, and the rest are left as exercises for the reader.
|
||||
The inherently typed representation is used.
|
||||
|
||||
\paragraph{Bisimulation: Relating reduction systems}
|
||||
Shows how to translate the language with ``let'' terms
|
||||
to the language without, representing a let as an application of an abstraction,
|
||||
and shows how to relate the source and target languages with a bisimulation.
|
||||
|
||||
\paragraph{Inference: Bidirectional type inference}
|
||||
Introduces bidirectional type inference, and applies it to convert from
|
||||
a representation with named variables and a separate typing relation
|
||||
to a representation de Bruijn indices with inherent types.
|
||||
|
||||
\paragraph{Untyped: Untyped calculus with full normalisation}
|
||||
As a variation on earlier themes, discusses an untyped (but inherently
|
||||
scoped) lambda calculus. Reduction is call-by-name over open terms,
|
||||
with full normalisation (including reduction under lambda terms). Emphasis
|
||||
is put on the correspondence between the structure of a term and
|
||||
evidence that it is in normal form.
|
||||
|
||||
\subsection*{Discussion}
|
||||
|
||||
PLFA and SF differ in several particulars. PLFA begins with a computationally
|
||||
complete language, PCF, while SF begins with a minimal language, simply-typed
|
||||
lambda calculus with booleans. PLFA does not include type annotations in terms,
|
||||
and uses bidirectional type inference, while SF has terms with unique types and
|
||||
uses type checking. SF also covers a simple imperative language with Hoare logic,
|
||||
subtyping, record types, mutable references, and normalisation none of which are
|
||||
treated by PLFA. PLFA covers an inherently-typed de Bruijn
|
||||
representation, bidirectional type inference, bisimulation, and an
|
||||
untyped call-by-value language with full normalisation, none of which
|
||||
are treated by SF.
|
||||
|
||||
SF has a third volume, written by Andrew Appel, on Verified Functional
|
||||
Algorithms. I'm not sufficiently familiar with that volume to have a view
|
||||
on whether it would be easy or hard to cover that material in Agda.
|
||||
|
||||
There is more material that would be desirable to include in PLFA
|
||||
which was not due to limits of time. In future years, PLFA may be
|
||||
extended to cover additional material, including mutable references,
|
||||
normalisation, System F, pure type systems, and denotational
|
||||
semantics. I'd especially like to include pure type systems as they
|
||||
provide the readers with a formal model close to the dependent types
|
||||
used in the book. My attempts so far to formalise pure type systems
|
||||
have proved challenging.
|
||||
|
||||
\section{Proofs in Agda and Coq}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/plfa-progress-1.png}
|
||||
\caption{PLFA, Progress (1/2)}
|
||||
\label{fig:plfa-progress-1}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[p]
|
||||
\includegraphics[width=\textwidth]{figures/plfa-progress-2.png}
|
||||
\includegraphics[width=\textwidth]{figures/plfa-progress-3a.png}
|
||||
\caption{PLFA, Progress (2/2)}
|
||||
\label{fig:plfa-progress-2}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/sf-progress-1.png}
|
||||
\caption{SF, Progress (1/2)}
|
||||
\label{fig:sf-progress-1}
|
||||
\end{figure}
|
||||
|
||||
\begin{figure}[t]
|
||||
\includegraphics[width=\textwidth]{figures/sf-progress-2.png}
|
||||
\caption{SF, Progress (2/2)}
|
||||
\label{fig:sf-progress-2}
|
||||
\end{figure}
|
||||
|
||||
% \begin{figure}[t]
|
||||
% \includegraphics[width=\textwidth]{figures/sf-progress-3.png}
|
||||
% \caption{SF, Progress (3/3)}
|
||||
% \label{fig:sf-progress-3}
|
||||
% \end{figure}
|
||||
|
||||
The introduction listed several reasons for preferring Agda over Coq.
|
||||
But Coq tactics enable more compact proofs. Would it be possible for
|
||||
PLFA to cover the same material as SF, or would the proofs
|
||||
balloon to unmanageable size?
|
||||
|
||||
As an experiment, I first rewrote SF's development of simply-typed
|
||||
lambda calculus (SF, Chapters Stlc and StlcProp) in Agda. I was a
|
||||
newbie to Agda, and translating the entire development, sticking as
|
||||
closely as possible to the development in SF, took me about two days.
|
||||
I was pleased to discover that the proofs remained about the same
|
||||
size.
|
||||
|
||||
There was also a pleasing surprise regarding the structure of the
|
||||
proofs. While most proofs in both SF and PLFA are carried out by
|
||||
induction over the evidence that a term is well typed, in SF the
|
||||
central proof, that substitution preserves types, is carried out by
|
||||
induction on terms, not evidence of typing, for a technical reason
|
||||
(the context is extended by a variable binding, and hence not
|
||||
sufficiently ``generic'' to work well with Coq's induction tactic). In
|
||||
Agda, I had no trouble formulating the same proof over evidence that
|
||||
the term is well typed, and didn't even notice SF's description of the
|
||||
issue until I was done.
|
||||
|
||||
The rest of the book was relatively easy to complete. The closest to
|
||||
an issue with proof size arose when proving that reduction is
|
||||
deterministic. There are 18 cases, one case per line. Ten of the
|
||||
cases deal with the situation where there are potentially two
|
||||
different reductions; each case is trivially shown to be
|
||||
impossible. Five of the ten cases are redundant, as they just involve
|
||||
switching the order of the arguments. I had to copy the cases
|
||||
suitably permuted. It would be preferable to reinvoke the proof on
|
||||
switched arguments, but this would not pass Agda's termination checker
|
||||
since swapping the arguments doesn't yield a recursive call on
|
||||
structurally smaller arguments. (I suspect tactics could cut down the
|
||||
proof significantly. I tried to compare with SF's proof that reduction
|
||||
is deterministic, but failed to find that proof.)
|
||||
|
||||
SF covers an imperative language with Hoare logic, culminating in
|
||||
code that takes an imperative programme suitably decorated with preconditions
|
||||
and postconditions and generates the necessary
|
||||
verification conditions. The conditions are then verified by a custom
|
||||
tactic, where any questions of arithmetic are resolved by the
|
||||
``omega'' tactic invoking a decision procedure. The entire
|
||||
exercise would be easy to repeat in Agda, save for the last step: I
|
||||
suspect Agda's automation would not be up to verifying the generated
|
||||
conditions, requiring tedious proofs by hand. However, I had already
|
||||
decided to omit Hoare logic in order to focus on lambda calculus.
|
||||
|
||||
To give a flavour of how the texts compare, I show the
|
||||
proof of progress for simply-typed lambda calculus from both texts.
|
||||
Figures~\ref{fig:plfa-progress-1} and \ref{fig:plfa-progress-2}
|
||||
are taken from PLFA, Chapter Properties,
|
||||
while Figures~\ref{fig:sf-progress-1} and \ref{fig:sf-progress-2}
|
||||
are taken from SF, Chapter StlcProp.
|
||||
Both texts are intended to be read online,
|
||||
and the figures were taken by grabbing bitmaps of the text as
|
||||
displayed in a browser.
|
||||
|
||||
PLFA puts the formal statements first, followed by informal explanation.
|
||||
PLFA introduces an auxiliary relation \texttt{Progress M} to capture
|
||||
progress; an exercise (not shown) asks the reader to show it isomorphic
|
||||
to the usual formulation with a disjunction and an existential.
|
||||
Layout is used to present the auxiliary relation in inference rule form.
|
||||
In Agda, any line beginning with two dashes is treated as a comment, making
|
||||
it easy to use a line of dashes to separate hypotheses from conclusion
|
||||
in inference rules. The proof is layed out carefully, with a neat
|
||||
indented structure to emphasise the case analysis, and all right-hand
|
||||
sides lined-up in the same column. My hope as an author is that students
|
||||
will read the formal proof first, and use it as a tabular guide
|
||||
to the informal explanation that follows.
|
||||
|
||||
SF puts the informal explanation first, followed by the formal proof.
|
||||
The text hides the formal proof script under an icon;
|
||||
the figures shows what appears when the icon is expanded.
|
||||
As a teacher I was aware that
|
||||
students might skip it on a first reading, and I would have to hope the
|
||||
students would return to it and step through it with an interactive
|
||||
tool in order to make it intelligible. I expect the students skipped over
|
||||
many such proofs. This particular proof forms the basis for a question
|
||||
of the mock exam and the past exams, so I expect most students will actually
|
||||
look at this one if not all the others.
|
||||
|
||||
Both Coq and Agda support interactive proof. Interaction in Coq is
|
||||
supported by Proof General, based on Emacs, or by CoqIDE, which
|
||||
provides an interactive development environment of a sort familiar to
|
||||
most students. Interaction in Agda is supported by an Emacs mode.
|
||||
|
||||
In Coq, interaction consists of stepping through a proof script, at
|
||||
each point examining the current goal and the variables currently in
|
||||
scope, and executing a new command in the script. Tactics are a whole
|
||||
sublanguage, which must be learned in addition to the langauge for
|
||||
expressing specifications. There are many tactics one can invoke in
|
||||
the script at each point; one menu in CoqIDE lists about one hundred
|
||||
tactics one might invoked, some in alphabetic submenus. A Coq
|
||||
script presents the specification proved and the tactics executed.
|
||||
Interaction is recorded in a script, which the students
|
||||
may step through at their leisure. SF contains some prose descriptions
|
||||
of stepping through scripts, but mainly contains scripts that students
|
||||
are encouraged to step through on their own.
|
||||
|
||||
In Agda, interaction consists of writing code with holes, at each
|
||||
point examining the current goal and the variables in scope, and
|
||||
typing code or executing an Emacs command. The number of commands
|
||||
available is much smaller than with Coq, the most important ones being
|
||||
to show the type of the hole and the types of the variables in scope;
|
||||
to check the code; to do a case analysis on a given variable; or to
|
||||
guess how to fill in the hole with constructors or variables in scope.
|
||||
An Agda proof consists of typed code. The interaction is \emph{not}
|
||||
recorded. Students may recreate it by commenting out bits of code and
|
||||
introducing a hole in their place. PLFA contains some prose descriptions
|
||||
of interactively building code, but mainly contains code that students
|
||||
can read. They may also introduce holes to interact with the code, but
|
||||
I expect this will be rarer than with SF.
|
||||
|
||||
SF encourages students to interact with all the scripts in the text.
|
||||
Trying to understand a Coq proof script without running it
|
||||
interactively is a bit like understanding a chess game by reading
|
||||
through the moves without benefit of a board, keeping it all in your
|
||||
head. In contrast, PLFA provides code that students can read.
|
||||
Understanding the code often requires working out the types, but
|
||||
(unlike executing a Coq proof script) this is often easy to do in your
|
||||
head; when it is not easy, students still have the option of
|
||||
interaction.
|
||||
|
||||
While students are keen to interact to create code, I have found they
|
||||
are reluctant to interact to understand code created by others. For
|
||||
this reason, I suspect this may make Agda a more suitable vehicle for
|
||||
teaching. Nate Foster suggests this hypothesis is ripe to be tested
|
||||
empirically, perhaps using techniques similar to those of
|
||||
\citet{Danas-et-al-2017}.
|
||||
|
||||
Neat layout of definitions such as that in
|
||||
Figure~\ref{fig:plfa-progress-2} in Emacs requires a monospaced font
|
||||
supporting all the necessary characters. Securing one has proved
|
||||
tricky. As of this writing, we use FreeMono, but it lacks a few
|
||||
characters (⦂ and ∎) which are loaded from fonts with a different
|
||||
width. Long arrows are necessarily more than a single character wide.
|
||||
Instead, we compose reduction —→ from an em dash — and an arrow →.
|
||||
Similarly for reflexive and transitive closure —↠.
|
||||
|
||||
\section{Progress + Preservation = Evaluation}
|
||||
|
||||
\begin{figure}
|
||||
\includegraphics[width=\textwidth]{figures/plfa-eval.png}
|
||||
\caption{PLFA, Evaluation}
|
||||
\label{fig:plfa-eval}
|
||||
\end{figure}
|
||||
|
||||
A standard approach to type soundness used by many texts,
|
||||
including SF and PLFA, is to prove progress and preservation,
|
||||
as first suggested by \citet{Wright-and-Felleisen-1994}.
|
||||
|
||||
\begin{theorem}[Progress] Given term $M$ and type $A$ such that
|
||||
$\emptyset \vdash M : A$ then either $M$ is a value or
|
||||
$M \longrightarrow N$ for some term $N$.
|
||||
\end{theorem}
|
||||
|
||||
\begin{theorem}[Preservation] Given terms $M$ and $N$ and type $A$
|
||||
such that $\emptyset \vdash M : A$ and $M \longrightarrow N$, then
|
||||
$\emptyset \vdash N : A$. \end{theorem}
|
||||
|
||||
A consequence is that when a term reduces to a value it retains
|
||||
the same type. Further, well-typed terms don't get stuck:
|
||||
that is, unable to reduce further but not yet reduced to a value.
|
||||
The formulation neatly accommodates the case of non-terminating
|
||||
reductions that never reach a value.
|
||||
|
||||
One useful by-product of the formal specification of a programming
|
||||
language may be a prototype implementation of that language. For
|
||||
instance, given a language specified by a reduction relation, such
|
||||
as lambda calculus, the prototype might accept a term and apply reductions
|
||||
to reduce it to a value. Typically, one might go to some extra work to
|
||||
create such a prototype. For instance, SF introduces a \texttt{normalize}
|
||||
tactic for this purpose. Some formal methods frameworks, such as
|
||||
Redex \citep{Felleisen-et-al-2009} and K \citep{Rosu-Serbanuta-2010},
|
||||
advertise as one of their advantages that they can generate
|
||||
a prototype from descriptions of the reduction rules.
|
||||
|
||||
I was therefore surprised to realise that any constructive proof of
|
||||
progress and preservation \emph{automatically} gives rise to such a
|
||||
prototype. The input is a term together with evidence the term is
|
||||
well-typed. (In the inherently-typed case, these are the same thing.)
|
||||
Progress determines whether we are done, or should take another step;
|
||||
preservation provides evidence that the new term is well-typed, so we
|
||||
may iterate. In a language with guaranteed termination, we cannot
|
||||
iterate forever, but there are a number of well-known techniques to
|
||||
address that issue; see, e.g., \citet{Bove-and-Capretta-2001},
|
||||
\citet{Capretta-2005}, or \citet{McBride-2015}.
|
||||
We use the simplest, similar to McBride's \emph{petrol-driven} (or
|
||||
\emph{step-indexed}) semantics: provide a maximum number of steps to
|
||||
execute; if that number proves insufficient, the evaluator returns the
|
||||
term it reached, and one can resume execution by providing a new
|
||||
number.
|
||||
|
||||
Such an evaluator from PLFA is shown in Figure~\ref{fig:plfa-eval},
|
||||
where (inspired by McBride and cryptocurrencies) the number of steps
|
||||
to execute is referred to as \emph{gas}. All of the example reduction
|
||||
sequences in PLFA were computed by the evaluator and then edited to
|
||||
improve readability; in addition, the text includes examples of
|
||||
running the evaluator with its unedited output.
|
||||
|
||||
It is immediately obvious that progress and preservation make it
|
||||
trivial to construct a prototype evaluator, and yet I cannot find such
|
||||
an observation in the literature nor mentioned in an introductory
|
||||
text. It does not appear in SF, nor in \citet{Harper-2016}. A plea
|
||||
to the Agda mailing list failed to turn up any prior mentions.
|
||||
The closest related observation I have seen in the published
|
||||
literature is that evaluators can be extracted from proofs of
|
||||
normalisation \citep{Berger-1993,Dagand-and-Scherer-2015}.
|
||||
|
||||
(Late addition: My plea to the Agda list eventually bore fruit. Oleg
|
||||
Kiselyov directed me to unpublished remarks on his web page where he
|
||||
uses the name \texttt{eval} for a proof of progress and notes ``the
|
||||
very proof of type soundness can be used to evaluate sample
|
||||
expressions'' \citet{Kiselyov-2009}.)
|
||||
|
||||
|
||||
\section{Inherent typing is golden}
|
||||
|
||||
The second part of PLFA first discusses two different approaches to
|
||||
modelling simply-typed lambda calculus. It first presents ``raw''
|
||||
terms with named variables and a separate typing relation and
|
||||
then shifts to inherently-typed terms with de Bruijn indices.
|
||||
Before writing the text, I had thought the two approaches
|
||||
complementary, with no clear winner. Now I am convinced that the
|
||||
inherently-typed approach is superior.
|
||||
|
||||
The clearest indication comes from counting lines of code.
|
||||
Stripping out examples and any proofs that appear in one but not the
|
||||
other, the development for raw terms takes 451 lines (216 lines of
|
||||
definitions and 235 lines for the proofs) and the development for
|
||||
inherently typed terms takes 275 lines (with definitions and proofs
|
||||
interleaved, as substitution cannot be defined without
|
||||
also showing it preserves types). We have 451 / 235 = 1.64, close
|
||||
to the golden ratio.
|
||||
|
||||
Another indication is expressive power. The approach with named
|
||||
variables and separate typing is restricted to substitution of one
|
||||
variable by a single closed term, while de Bruijn indices with
|
||||
inherent typing support simultaneous substitution of all variables by
|
||||
open terms, using a pleasing formulation due to \citet{McBride-2005},
|
||||
inspired by \citet{Goguen-and-McKinna-1997} and described
|
||||
in \citet{Allais-et-al-2017}. In fact, I managed to extend
|
||||
McBride's approach to support raw terms with named variables, but the
|
||||
resulting code was too long and too complex for use in an introductory
|
||||
text, requiring 695 lines of code---more than the total for the other
|
||||
two approaches combined.
|
||||
|
||||
The text develops both approaches because named variables with
|
||||
separate typing is more familiar, and placing de Bruijn indices and
|
||||
inherent typing first would lead to a steep learning curve. By
|
||||
presenting the more long-winded but less powerful approach first,
|
||||
students can see for themselves the advantages of de Bruijn indices
|
||||
with inherent typing.
|
||||
|
||||
There are actually four possible designs, as the choice of named
|
||||
variables vs de Bruijn indices, and the choice of raw vs
|
||||
inherently-typed terms may be made independently. There are synergies
|
||||
beween the two. Manipulation of de Bruijn indices can be notoriously
|
||||
error-prone without inherent-typing to give assurance of correctness.
|
||||
In inherent typing with named variables, simultaneous substitution by
|
||||
open terms remains difficult.
|
||||
|
||||
The benefits of replacing raw typing by inherent are well
|
||||
known to some. The technique was introduced by
|
||||
\citet{Altenkirch-and-Reus-1999}, and widely used elsewhere,
|
||||
notably by \citet{Chapman-2009} and \citet{Allais-et-al-2017}.
|
||||
I'm grateful to David Darais for bringing it to my attention.
|
||||
|
||||
|
||||
\section{Conclusion}
|
||||
|
||||
I look forward to experience teaching from the new text,
|
||||
and encourage others to use it too. Please comment!
|
||||
|
||||
|
||||
\paragraph{Acknowledgements}
|
||||
|
||||
A special thank you to my coauthor, Wen Kokke. For inventing ideas on
|
||||
which PLFA is based, and for hand-holding, many thanks to Conor
|
||||
McBride, James McKinna, Ulf Norell, and Andreas Abel. For showing me
|
||||
how much more compact it is to avoid raw terms, thanks to David
|
||||
Darais. For inspiring my work by writing SF, thanks to Benjamin
|
||||
Pierce and his coauthors. For comments on a draft of this paper, an
|
||||
extra thank you to James McKinna, Ulf Norell, Andreas Abel, and
|
||||
Benjamin Pierce.
|
||||
|
||||
\bibliographystyle{plainnat}
|
||||
%\bibliographystyle{splncsnat.bst}
|
||||
\bibliography{PLFA}
|
||||
|
||||
|
||||
|
||||
\end{document}
|
||||
|
||||
|
||||
691
papers/scp/latex/agda.sty
Normal file
691
papers/scp/latex/agda.sty
Normal file
|
|
@ -0,0 +1,691 @@
|
|||
% ----------------------------------------------------------------------
|
||||
% Some useful commands when doing highlighting of Agda code in LaTeX.
|
||||
% ----------------------------------------------------------------------
|
||||
|
||||
\ProvidesPackage{agda}
|
||||
|
||||
\RequirePackage{ifxetex, ifluatex, xifthen, xcolor, polytable, etoolbox,
|
||||
calc, environ}
|
||||
|
||||
% https://tex.stackexchange.com/questions/47576/combining-ifxetex-and-ifluatex-with-the-logical-or-operation
|
||||
\newif\ifxetexorluatex
|
||||
\ifxetex
|
||||
\xetexorluatextrue
|
||||
\else
|
||||
\ifluatex
|
||||
\xetexorluatextrue
|
||||
\else
|
||||
\xetexorluatexfalse
|
||||
\fi
|
||||
\fi
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Options
|
||||
|
||||
\DeclareOption{bw} {\newcommand{\AgdaColourScheme}{bw}}
|
||||
\DeclareOption{conor}{\newcommand{\AgdaColourScheme}{conor}}
|
||||
|
||||
\newif\if@AgdaEnableReferences\@AgdaEnableReferencesfalse
|
||||
\DeclareOption{references}{
|
||||
\@AgdaEnableReferencestrue
|
||||
}
|
||||
|
||||
\newif\if@AgdaEnableLinks\@AgdaEnableLinksfalse
|
||||
\DeclareOption{links}{
|
||||
\@AgdaEnableLinkstrue
|
||||
}
|
||||
|
||||
% If the "nofontsetup" option is used, then the package does not
|
||||
% select any fonts, and it does not change the font encoding.
|
||||
\newif\if@AgdaSetupFonts\@AgdaSetupFontstrue
|
||||
\DeclareOption{nofontsetup}{
|
||||
\@AgdaSetupFontsfalse
|
||||
}
|
||||
|
||||
% If the "noinputencodingsetup" option is used, then the package does
|
||||
% not change the input encoding, and it does not load the `ucs`
|
||||
% package.
|
||||
\newif\if@AgdaSetupInputEncoding\@AgdaSetupInputEncodingtrue
|
||||
\DeclareOption{noinputencodingsetup}{
|
||||
\@AgdaSetupInputEncodingfalse
|
||||
}
|
||||
|
||||
\ProcessOptions\relax
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Input encoding setup
|
||||
|
||||
\if@AgdaSetupInputEncoding
|
||||
\ifxetexorluatex
|
||||
|
||||
\providecommand{\DeclareUnicodeCharacter}[2]{\relax}
|
||||
|
||||
\else
|
||||
|
||||
\RequirePackage{ucs}
|
||||
\RequirePackage[utf8x]{inputenc}
|
||||
|
||||
\fi
|
||||
\fi
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Font setup
|
||||
|
||||
\tracinglostchars=2 % If the font is missing some symbol, then say
|
||||
% so in the compilation output.
|
||||
|
||||
\if@AgdaSetupFonts
|
||||
% XeLaTeX or LuaLaTeX
|
||||
\ifxetexorluatex
|
||||
|
||||
% Hack to get the amsthm package working.
|
||||
% https://tex.stackexchange.com/questions/130491/xelatex-error-paragraph-ended-before-tempa-was-complete
|
||||
\let\AgdaOpenBracket\[\let\AgdaCloseBracket\]
|
||||
\RequirePackage{fontspec}
|
||||
\let\[\AgdaOpenBracket\let\]\AgdaCloseBracket
|
||||
\RequirePackage{unicode-math}
|
||||
|
||||
\setmainfont
|
||||
[ Ligatures = TeX
|
||||
, BoldItalicFont = xits-bolditalic.otf
|
||||
, BoldFont = xits-bold.otf
|
||||
, ItalicFont = xits-italic.otf
|
||||
]
|
||||
{xits-regular.otf}
|
||||
|
||||
\setmathfont{xits-math.otf}
|
||||
\setmonofont[Mapping=tex-text]{FreeMono.otf}
|
||||
|
||||
% Make mathcal and mathscr appear as different.
|
||||
% https://tex.stackexchange.com/questions/120065/xetex-what-happened-to-mathcal-and-mathscr
|
||||
\setmathfont[range={\mathcal,\mathbfcal},StylisticSet=1]{xits-math.otf}
|
||||
\setmathfont[range=\mathscr]{xits-math.otf}
|
||||
|
||||
% pdfLaTeX
|
||||
\else
|
||||
|
||||
% https://tex.stackexchange.com/questions/1774/how-to-insert-pipe-symbol-in-latex
|
||||
\RequirePackage[T1]{fontenc}
|
||||
|
||||
\RequirePackage{amsfonts, amssymb}
|
||||
\RequirePackage[safe]{tipa} % See page 12 of the tipa manual for what
|
||||
% safe does.
|
||||
|
||||
\fi
|
||||
\fi
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Colour schemes.
|
||||
|
||||
\providecommand{\AgdaColourScheme}{standard}
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% References to code (needs additional post-processing of tex files to
|
||||
% work, see wiki for details).
|
||||
|
||||
\if@AgdaEnableReferences
|
||||
\RequirePackage{catchfilebetweentags, xstring}
|
||||
\newcommand{\AgdaRef}[2][]{%
|
||||
\StrSubstitute{#2}{\_}{AgdaUnderscore}[\tmp]%
|
||||
\ifthenelse{\isempty{#1}}%
|
||||
{\ExecuteMetaData{AgdaTag-\tmp}}%
|
||||
{\ExecuteMetaData{#1}{AgdaTag-\tmp}}
|
||||
}
|
||||
\fi
|
||||
|
||||
\providecommand{\AgdaRef}[2][]{#2}
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Links (only done if the option is passed and the user has loaded the
|
||||
% hyperref package).
|
||||
|
||||
\if@AgdaEnableLinks
|
||||
\@ifpackageloaded{hyperref}{
|
||||
|
||||
% List that holds added targets.
|
||||
\newcommand{\AgdaList}[0]{}
|
||||
|
||||
\newtoggle{AgdaIsElem}
|
||||
\newcounter{AgdaIndex}
|
||||
\newcommand{\AgdaLookup}[3]{%
|
||||
\togglefalse{AgdaIsElem}%
|
||||
\setcounter{AgdaIndex}{0}%
|
||||
\renewcommand*{\do}[1]{%
|
||||
\ifstrequal{#1}{##1}%
|
||||
{\toggletrue{AgdaIsElem}\listbreak}%
|
||||
{\stepcounter{AgdaIndex}}}%
|
||||
\dolistloop{\AgdaList}%
|
||||
\iftoggle{AgdaIsElem}{#2}{#3}%
|
||||
}
|
||||
|
||||
\newcommand*{\AgdaTargetHelper}[1]{%
|
||||
\AgdaLookup{#1}%
|
||||
{\PackageError{agda}{``#1'' used as target more than once}%
|
||||
{Overloaded identifiers and links do not%
|
||||
work well, consider using unique%
|
||||
\MessageBreak identifiers instead.}%
|
||||
}%
|
||||
{\listadd{\AgdaList}{#1}%
|
||||
\hypertarget{Agda\theAgdaIndex}{}%
|
||||
}%
|
||||
}
|
||||
|
||||
\newcommand{\AgdaTarget}[1]{\forcsvlist{\AgdaTargetHelper}{#1}}
|
||||
|
||||
\newcommand{\AgdaLink}[1]{%
|
||||
\AgdaLookup{#1}%
|
||||
{\hyperlink{Agda\theAgdaIndex}{#1}}%
|
||||
{#1}%
|
||||
}
|
||||
}{\PackageError{agda}{Load the hyperref package before the agda package}{}}
|
||||
\fi
|
||||
|
||||
\providecommand{\AgdaTarget}[1]{}
|
||||
\providecommand{\AgdaLink}[1]{#1}
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Font styles.
|
||||
|
||||
\ifxetexorluatex
|
||||
\newcommand{\AgdaFontStyle}[1]{\ensuremath{\mathsf{#1}}}
|
||||
\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
|
||||
\newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
|
||||
}{
|
||||
\newcommand{\AgdaKeywordFontStyle}[1]{\ensuremath{\mathsf{#1}}}
|
||||
}
|
||||
\newcommand{\AgdaStringFontStyle}[1]{\ensuremath{\texttt{#1}}}
|
||||
\newcommand{\AgdaCommentFontStyle}[1]{\ensuremath{\texttt{#1}}}
|
||||
\newcommand{\AgdaBoundFontStyle}[1]{\ensuremath{\mathit{#1}}}
|
||||
|
||||
\else
|
||||
\newcommand{\AgdaFontStyle}[1]{\textsf{#1}}
|
||||
\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
|
||||
\newcommand{\AgdaKeywordFontStyle}[1]{\underline{#1}}
|
||||
}{
|
||||
\newcommand{\AgdaKeywordFontStyle}[1]{\textsf{#1}}
|
||||
}
|
||||
\newcommand{\AgdaStringFontStyle}[1]{\texttt{#1}}
|
||||
\newcommand{\AgdaCommentFontStyle}[1]{\texttt{#1}}
|
||||
\newcommand{\AgdaBoundFontStyle}[1]{\textit{#1}}
|
||||
\fi
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Colours.
|
||||
|
||||
% ----------------------------------
|
||||
% The black and white colour scheme.
|
||||
\ifthenelse{\equal{\AgdaColourScheme}{bw}}{
|
||||
|
||||
% Aspect colours.
|
||||
\definecolor{AgdaComment} {HTML}{000000}
|
||||
\definecolor{AgdaOption} {HTML}{000000}
|
||||
\definecolor{AgdaKeyword} {HTML}{000000}
|
||||
\definecolor{AgdaString} {HTML}{000000}
|
||||
\definecolor{AgdaNumber} {HTML}{000000}
|
||||
\definecolor{AgdaSymbol} {HTML}{000000}
|
||||
\definecolor{AgdaPrimitiveType}{HTML}{000000}
|
||||
|
||||
% NameKind colours.
|
||||
\definecolor{AgdaBound} {HTML}{000000}
|
||||
\definecolor{AgdaInductiveConstructor} {HTML}{000000}
|
||||
\definecolor{AgdaCoinductiveConstructor}{HTML}{000000}
|
||||
\definecolor{AgdaDatatype} {HTML}{000000}
|
||||
\definecolor{AgdaField} {HTML}{000000}
|
||||
\definecolor{AgdaFunction} {HTML}{000000}
|
||||
\definecolor{AgdaMacro} {HTML}{000000}
|
||||
\definecolor{AgdaModule} {HTML}{000000}
|
||||
\definecolor{AgdaPostulate} {HTML}{000000}
|
||||
\definecolor{AgdaPrimitive} {HTML}{000000}
|
||||
\definecolor{AgdaRecord} {HTML}{000000}
|
||||
\definecolor{AgdaArgument} {HTML}{000000}
|
||||
|
||||
% Other aspect colours.
|
||||
\definecolor{AgdaDottedPattern} {HTML}{000000}
|
||||
\definecolor{AgdaUnsolvedMeta} {HTML}{D3D3D3}
|
||||
\definecolor{AgdaTerminationProblem}{HTML}{BEBEBE}
|
||||
\definecolor{AgdaIncompletePattern} {HTML}{D3D3D3}
|
||||
\definecolor{AgdaError} {HTML}{696969}
|
||||
|
||||
% Misc.
|
||||
\definecolor{AgdaHole} {HTML}{BEBEBE}
|
||||
|
||||
% ----------------------------------
|
||||
% Conor McBride's colour scheme.
|
||||
}{ \ifthenelse{\equal{\AgdaColourScheme}{conor}}{
|
||||
|
||||
% Aspect colours.
|
||||
\definecolor{AgdaComment} {HTML}{B22222}
|
||||
\definecolor{AgdaOption} {HTML}{000000}
|
||||
\definecolor{AgdaKeyword} {HTML}{000000}
|
||||
\definecolor{AgdaString} {HTML}{000000}
|
||||
\definecolor{AgdaNumber} {HTML}{000000}
|
||||
\definecolor{AgdaSymbol} {HTML}{000000}
|
||||
\definecolor{AgdaPrimitiveType}{HTML}{0000CD}
|
||||
|
||||
% NameKind colours.
|
||||
\definecolor{AgdaBound} {HTML}{A020F0}
|
||||
\definecolor{AgdaInductiveConstructor} {HTML}{8B0000}
|
||||
\definecolor{AgdaCoinductiveConstructor}{HTML}{8B0000}
|
||||
\definecolor{AgdaDatatype} {HTML}{0000CD}
|
||||
\definecolor{AgdaField} {HTML}{8B0000}
|
||||
\definecolor{AgdaFunction} {HTML}{006400}
|
||||
\definecolor{AgdaMacro} {HTML}{006400}
|
||||
\definecolor{AgdaModule} {HTML}{006400}
|
||||
\definecolor{AgdaPostulate} {HTML}{006400}
|
||||
\definecolor{AgdaPrimitive} {HTML}{006400}
|
||||
\definecolor{AgdaRecord} {HTML}{0000CD}
|
||||
\definecolor{AgdaArgument} {HTML}{404040}
|
||||
|
||||
% Other aspect colours.
|
||||
\definecolor{AgdaDottedPattern} {HTML}{000000}
|
||||
\definecolor{AgdaUnsolvedMeta} {HTML}{FFD700}
|
||||
\definecolor{AgdaTerminationProblem}{HTML}{FF0000}
|
||||
\definecolor{AgdaIncompletePattern} {HTML}{A020F0}
|
||||
\definecolor{AgdaError} {HTML}{F4A460}
|
||||
|
||||
% Misc.
|
||||
\definecolor{AgdaHole} {HTML}{9DFF9D}
|
||||
|
||||
% ----------------------------------
|
||||
% The standard colour scheme.
|
||||
}{
|
||||
% Aspect colours.
|
||||
\definecolor{AgdaComment} {HTML}{B22222}
|
||||
\definecolor{AgdaOption} {HTML}{000000}
|
||||
\definecolor{AgdaKeyword} {HTML}{CD6600}
|
||||
\definecolor{AgdaString} {HTML}{B22222}
|
||||
\definecolor{AgdaNumber} {HTML}{A020F0}
|
||||
\definecolor{AgdaSymbol} {HTML}{404040}
|
||||
\definecolor{AgdaPrimitiveType}{HTML}{0000CD}
|
||||
|
||||
% NameKind colours.
|
||||
\definecolor{AgdaBound} {HTML}{000000}
|
||||
\definecolor{AgdaInductiveConstructor} {HTML}{008B00}
|
||||
\definecolor{AgdaCoinductiveConstructor}{HTML}{8B7500}
|
||||
\definecolor{AgdaDatatype} {HTML}{0000CD}
|
||||
\definecolor{AgdaField} {HTML}{EE1289}
|
||||
\definecolor{AgdaFunction} {HTML}{0000CD}
|
||||
\definecolor{AgdaMacro} {HTML}{458B74}
|
||||
\definecolor{AgdaModule} {HTML}{A020F0}
|
||||
\definecolor{AgdaPostulate} {HTML}{0000CD}
|
||||
\definecolor{AgdaPrimitive} {HTML}{0000CD}
|
||||
\definecolor{AgdaRecord} {HTML}{0000CD}
|
||||
\definecolor{AgdaArgument} {HTML}{404040}
|
||||
|
||||
% Other aspect colours.
|
||||
\definecolor{AgdaDottedPattern} {HTML}{000000}
|
||||
\definecolor{AgdaUnsolvedMeta} {HTML}{FFFF00}
|
||||
\definecolor{AgdaTerminationProblem}{HTML}{FFA07A}
|
||||
\definecolor{AgdaIncompletePattern} {HTML}{F5DEB3}
|
||||
\definecolor{AgdaError} {HTML}{FF0000}
|
||||
|
||||
% Misc.
|
||||
\definecolor{AgdaHole} {HTML}{9DFF9D}
|
||||
}}
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% Commands.
|
||||
|
||||
\newcommand{\AgdaNoSpaceMath}[1]
|
||||
{\begingroup\thickmuskip=0mu\medmuskip=0mu#1\endgroup}
|
||||
|
||||
% Aspect commands.
|
||||
\newcommand{\AgdaComment} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaComment}{#1}}}}
|
||||
\newcommand{\AgdaOption} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaCommentFontStyle{\textcolor{AgdaOption}{#1}}}}
|
||||
\newcommand{\AgdaKeyword} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaKeywordFontStyle{\textcolor{AgdaKeyword}{#1}}}}
|
||||
\newcommand{\AgdaString} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaStringFontStyle{\textcolor{AgdaString}{#1}}}}
|
||||
\newcommand{\AgdaNumber} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaNumber}{#1}}}}
|
||||
\newcommand{\AgdaSymbol} [1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaSymbol}{#1}}}}
|
||||
\newcommand{\AgdaPrimitiveType}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitiveType}{#1}}}}
|
||||
% Note that, in code generated by the LaTeX backend, \AgdaOperator is
|
||||
% always applied to a NameKind command.
|
||||
\newcommand{\AgdaOperator} [1]{#1}
|
||||
|
||||
% NameKind commands.
|
||||
|
||||
% The user can control the typesetting of (certain) individual tokens
|
||||
% by redefining the following command. The first argument is the token
|
||||
% and the second argument the thing to be typeset (sometimes just the
|
||||
% token, sometimes \AgdaLink{<the token>}). Example:
|
||||
%
|
||||
% \usepackage{ifthen}
|
||||
%
|
||||
% % Insert extra space before some tokens.
|
||||
% \DeclareRobustCommand{\AgdaFormat}[2]{%
|
||||
% \ifthenelse{
|
||||
% \equal{#1}{≡⟨} \OR
|
||||
% \equal{#1}{≡⟨⟩} \OR
|
||||
% \equal{#1}{∎}
|
||||
% }{\ }{}#2}
|
||||
%
|
||||
% Note the use of \DeclareRobustCommand.
|
||||
|
||||
\newcommand{\AgdaFormat}[2]{#2}
|
||||
|
||||
\newcommand{\AgdaBound}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaBound}{\AgdaFormat{#1}{#1}}}}}
|
||||
\newcommand{\AgdaInductiveConstructor}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaInductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaCoinductiveConstructor}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaCoinductiveConstructor}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaDatatype}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaDatatype}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaField}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaField}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaFunction}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaFunction}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaMacro}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaMacro}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaModule}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaModule}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaPostulate}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPostulate}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaPrimitive}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaPrimitive}{\AgdaFormat{#1}{#1}}}}}
|
||||
\newcommand{\AgdaRecord}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaFontStyle{\textcolor{AgdaRecord}{\AgdaFormat{#1}{\AgdaLink{#1}}}}}}
|
||||
\newcommand{\AgdaArgument}[1]
|
||||
{\AgdaNoSpaceMath{\AgdaBoundFontStyle{\textcolor{AgdaArgument}{\AgdaFormat{#1}{#1}}}}}
|
||||
|
||||
% Other aspect commands.
|
||||
\newcommand{\AgdaFixityOp} [1]{\AgdaNoSpaceMath{$#1$}}
|
||||
\newcommand{\AgdaDottedPattern} [1]{\textcolor{AgdaDottedPattern}{#1}}
|
||||
\newcommand{\AgdaUnsolvedMeta} [1]
|
||||
{\AgdaFontStyle{\colorbox{AgdaUnsolvedMeta}{#1}}}
|
||||
\newcommand{\AgdaTerminationProblem}[1]
|
||||
{\AgdaFontStyle{\colorbox{AgdaTerminationProblem}{#1}}}
|
||||
\newcommand{\AgdaIncompletePattern} [1]{\colorbox{AgdaIncompletePattern}{#1}}
|
||||
\newcommand{\AgdaError} [1]
|
||||
{\AgdaFontStyle{\textcolor{AgdaError}{\underline{#1}}}}
|
||||
\newcommand{\AgdaCatchallClause} [1]{#1} % feel free to change this
|
||||
|
||||
% Used to hide code from LaTeX.
|
||||
%
|
||||
% Note that this macro has been deprecated in favour of giving the
|
||||
% hide argument to the code environment.
|
||||
\long\def\AgdaHide#1{\ignorespaces}
|
||||
|
||||
% Misc.
|
||||
\newcommand{\AgdaHole}[1]{\colorbox{AgdaHole}{#1}}
|
||||
|
||||
% ----------------------------------------------------------------------
|
||||
% The code environment.
|
||||
|
||||
\newcommand{\AgdaCodeStyle}{}
|
||||
% \newcommand{\AgdaCodeStyle}{\tiny}
|
||||
|
||||
\ifdefined\mathindent
|
||||
{}
|
||||
\else
|
||||
\newdimen\mathindent\mathindent\leftmargini
|
||||
\fi
|
||||
|
||||
% Adds the given amount of vertical space and starts a new line.
|
||||
%
|
||||
% The implementation comes from lhs2TeX's polycode.fmt, written by
|
||||
% Andres Löh.
|
||||
\newcommand{\Agda@NewlineWithVerticalSpace}[1]{%
|
||||
{\parskip=0pt\parindent=0pt\par\vskip #1\noindent}}
|
||||
|
||||
% Should there be space around code?
|
||||
\newboolean{Agda@SpaceAroundCode}
|
||||
|
||||
% Use this command to avoid extra space around code blocks.
|
||||
\newcommand{\AgdaNoSpaceAroundCode}{%
|
||||
\setboolean{Agda@SpaceAroundCode}{false}}
|
||||
|
||||
% Use this command to include extra space around code blocks.
|
||||
\newcommand{\AgdaSpaceAroundCode}{%
|
||||
\setboolean{Agda@SpaceAroundCode}{true}}
|
||||
|
||||
% By default space is inserted around code blocks.
|
||||
\AgdaSpaceAroundCode{}
|
||||
|
||||
% Sometimes one might want to break up a code block into multiple
|
||||
% pieces, but keep code in different blocks aligned with respect to
|
||||
% each other. Then one can use the AgdaAlign environment. Example
|
||||
% usage:
|
||||
%
|
||||
% \begin{AgdaAlign}
|
||||
% \begin{code}
|
||||
% code
|
||||
% code (more code)
|
||||
% \end{code}
|
||||
% Explanation...
|
||||
% \begin{code}
|
||||
% aligned with "code"
|
||||
% code (aligned with (more code))
|
||||
% \end{code}
|
||||
% \end{AgdaAlign}
|
||||
%
|
||||
% Note that AgdaAlign environments should not be nested.
|
||||
%
|
||||
% Sometimes one might also want to hide code in the middle of a code
|
||||
% block. This can be accomplished in the following way:
|
||||
%
|
||||
% \begin{AgdaAlign}
|
||||
% \begin{code}
|
||||
% visible
|
||||
% \end{code}
|
||||
% \begin{code}[hide]
|
||||
% hidden
|
||||
% \end{code}
|
||||
% \begin{code}
|
||||
% visible
|
||||
% \end{code}
|
||||
% \end{AgdaAlign}
|
||||
%
|
||||
% However, the result may be ugly: extra space is perhaps inserted
|
||||
% around the code blocks.
|
||||
%
|
||||
% The AgdaSuppressSpace environment ensures that extra space is only
|
||||
% inserted before the first code block, and after the last one (but
|
||||
% not if \AgdaNoSpaceAroundCode{} is used). Example usage:
|
||||
%
|
||||
% \begin{AgdaAlign}
|
||||
% \begin{code}
|
||||
% code
|
||||
% more code
|
||||
% \end{code}
|
||||
% Explanation...
|
||||
% \begin{AgdaSuppressSpace}
|
||||
% \begin{code}
|
||||
% aligned with "code"
|
||||
% aligned with "more code"
|
||||
% \end{code}
|
||||
% \begin{code}[hide]
|
||||
% hidden code
|
||||
% \end{code}
|
||||
% \begin{code}
|
||||
% also aligned with "more code"
|
||||
% \end{code}
|
||||
% \end{AgdaSuppressSpace}
|
||||
% \end{AgdaAlign}
|
||||
%
|
||||
% Note that AgdaSuppressSpace environments should not be nested.
|
||||
%
|
||||
% There is also a combined environment, AgdaMultiCode, that combines
|
||||
% the effects of AgdaAlign and AgdaSuppressSpace.
|
||||
|
||||
% The number of the current/next code block (excluding hidden ones).
|
||||
\newcounter{Agda@Current}
|
||||
\setcounter{Agda@Current}{0}
|
||||
|
||||
% The number of the previous code block (excluding hidden ones), used
|
||||
% locally in \Agda@SuppressEnd.
|
||||
\newcounter{Agda@Previous}
|
||||
|
||||
% Is AgdaAlign active?
|
||||
\newboolean{Agda@Align}
|
||||
\setboolean{Agda@Align}{false}
|
||||
|
||||
% The number of the first code block (if any) in a given AgdaAlign
|
||||
% environment.
|
||||
\newcounter{Agda@AlignStart}
|
||||
|
||||
\newcommand{\Agda@AlignStart}{%
|
||||
\ifthenelse{\boolean{Agda@Align}}{%
|
||||
\PackageError{agda}{Nested AgdaAlign environments}{%
|
||||
AgdaAlign and AgdaMultiCode environments must not be
|
||||
nested.}}{%
|
||||
\setboolean{Agda@Align}{true}%
|
||||
\setcounter{Agda@AlignStart}{\value{Agda@Current}}}}
|
||||
|
||||
\newcommand{\Agda@AlignEnd}{\setboolean{Agda@Align}{false}}
|
||||
|
||||
\newenvironment{AgdaAlign}{%
|
||||
\Agda@AlignStart{}}{%
|
||||
\Agda@AlignEnd{}%
|
||||
\ignorespacesafterend}
|
||||
|
||||
% Is AgdaSuppressSpace active?
|
||||
\newboolean{Agda@Suppress}
|
||||
\setboolean{Agda@Suppress}{false}
|
||||
|
||||
% The number of the first code block (if any) in a given
|
||||
% AgdaSuppressSpace environment.
|
||||
\newcounter{Agda@SuppressStart}
|
||||
|
||||
% Does a "do not suppress space after" label exist for the current
|
||||
% code block? (This boolean is used locally in the code environment's
|
||||
% implementation.)
|
||||
\newboolean{Agda@DoNotSuppressSpaceAfter}
|
||||
|
||||
\newcommand{\Agda@SuppressStart}{%
|
||||
\ifthenelse{\boolean{Agda@Suppress}}{%
|
||||
\PackageError{agda}{Nested AgdaSuppressSpace environments}{%
|
||||
AgdaSuppressSpace and AgdaMultiCode environments must not be
|
||||
nested.}}{%
|
||||
\setboolean{Agda@Suppress}{true}%
|
||||
\setcounter{Agda@SuppressStart}{\value{Agda@Current}}}}
|
||||
|
||||
% Marks the given code block as one that space should not be
|
||||
% suppressed after (if AgdaSpaceAroundCode and AgdaSuppressSpace are
|
||||
% both active).
|
||||
\newcommand{\Agda@DoNotSuppressSpaceAfter}[1]{%
|
||||
% The use of labels is intended to ensure that LaTeX will provide a
|
||||
% warning if the document needs to be recompiled.
|
||||
\label{Agda@DoNotSuppressSpaceAfter@#1}}
|
||||
|
||||
\newcommand{\Agda@SuppressEnd}{%
|
||||
\ifthenelse{\value{Agda@SuppressStart} = \value{Agda@Current}}{}{%
|
||||
% Mark the previous code block in the .aux file.
|
||||
\setcounter{Agda@Previous}{\theAgda@Current-1}%
|
||||
\immediate\write\@auxout{%
|
||||
\noexpand\Agda@DoNotSuppressSpaceAfter{\theAgda@Previous}}}%
|
||||
\setboolean{Agda@Suppress}{false}}
|
||||
|
||||
\newenvironment{AgdaSuppressSpace}{%
|
||||
\Agda@SuppressStart{}}{%
|
||||
\Agda@SuppressEnd{}%
|
||||
\ignorespacesafterend}
|
||||
|
||||
\newenvironment{AgdaMultiCode}{%
|
||||
\Agda@AlignStart{}%
|
||||
\Agda@SuppressStart{}}{%
|
||||
\Agda@SuppressEnd{}%
|
||||
\Agda@AlignEnd{}%
|
||||
\ignorespacesafterend}
|
||||
|
||||
% Vertical space used for empty lines. By default \baselineskip.
|
||||
\newlength{\AgdaEmptySkip}
|
||||
\setlength{\AgdaEmptySkip}{\baselineskip}
|
||||
|
||||
% Extra space to be inserted for empty lines (the difference between
|
||||
% \AgdaEmptySkip and \baselineskip). Used internally.
|
||||
\newlength{\AgdaEmptyExtraSkip}
|
||||
|
||||
% The code environment.
|
||||
%
|
||||
% Code can be hidden by writing \begin{code}[hide].
|
||||
%
|
||||
% The implementation is based on plainhscode in lhs2TeX's
|
||||
% polycode.fmt, written by Andres Löh.
|
||||
\NewEnviron{code}[1][]{%
|
||||
% Conditionally hide the code.
|
||||
\ifthenelse{\equal{#1}{hide}}{}{%
|
||||
%
|
||||
% Conditionally emit space before the code block. Unconditionally
|
||||
% switch to a new line.
|
||||
\ifthenelse{\boolean{Agda@SpaceAroundCode} \and%
|
||||
\(\not \boolean{Agda@Suppress} \or%
|
||||
\value{Agda@SuppressStart} = \value{Agda@Current}\)}{%
|
||||
\Agda@NewlineWithVerticalSpace{\abovedisplayskip}}{%
|
||||
\Agda@NewlineWithVerticalSpace{0pt}}%
|
||||
%
|
||||
% Indent the entire code block.
|
||||
\advance\leftskip\mathindent%
|
||||
%
|
||||
% The code's style can be customised.
|
||||
\AgdaCodeStyle%
|
||||
%
|
||||
% Used to control the height of empty lines.
|
||||
\setlength{\AgdaEmptyExtraSkip}{\AgdaEmptySkip - \baselineskip}%
|
||||
%
|
||||
% The environment used to handle indentation (of individual lines)
|
||||
% and alignment.
|
||||
\begin{pboxed}%
|
||||
%
|
||||
% Conditionally preserve alignment between code blocks.
|
||||
\ifthenelse{\boolean{Agda@Align}}{%
|
||||
\ifthenelse{\value{Agda@AlignStart} = \value{Agda@Current}}{%
|
||||
\savecolumns}{%
|
||||
\restorecolumns}}{}%
|
||||
%
|
||||
% The code.
|
||||
\BODY%
|
||||
\end{pboxed}%
|
||||
%
|
||||
% Does the label Agda@DoNotSuppressAfter@<current code block
|
||||
% number> exist?
|
||||
\ifcsdef{r@Agda@DoNotSuppressSpaceAfter@\theAgda@Current}{%
|
||||
\setboolean{Agda@DoNotSuppressSpaceAfter}{true}}{%
|
||||
\setboolean{Agda@DoNotSuppressSpaceAfter}{false}}%
|
||||
%
|
||||
% Conditionally emit space after the code block. Unconditionally
|
||||
% switch to a new line.
|
||||
\ifthenelse{\boolean{Agda@SpaceAroundCode} \and%
|
||||
\(\not \boolean{Agda@Suppress} \or%
|
||||
\boolean{Agda@DoNotSuppressSpaceAfter}\)}{%
|
||||
\Agda@NewlineWithVerticalSpace{\belowdisplayskip}}{%
|
||||
\Agda@NewlineWithVerticalSpace{0pt}}%
|
||||
%
|
||||
% Step the code block counter, but only for non-hidden code.
|
||||
\stepcounter{Agda@Current}}}
|
||||
|
||||
% Space inserted after tokens.
|
||||
\newcommand{\AgdaSpace}{ }
|
||||
|
||||
% Space inserted to indent something.
|
||||
\newcommand{\AgdaIndentSpace}{\AgdaSpace{}$\;\;$}
|
||||
|
||||
% Default column for polytable.
|
||||
\defaultcolumn{@{}l@{\AgdaSpace{}}}
|
||||
|
||||
% \AgdaIndent expects a non-negative integer as its only argument.
|
||||
% This integer should be the distance, in code blocks, to the thing
|
||||
% relative to which the text is indented.
|
||||
%
|
||||
% The default implementation only indents if the thing that the text
|
||||
% is indented relative to exists in the same code block or is wrapped
|
||||
% in the same AgdaAlign or AgdaMultiCode environment.
|
||||
\newcommand{\AgdaIndent}[1]{%
|
||||
\ifthenelse{#1 = 0
|
||||
\or
|
||||
\( \boolean{Agda@Align}
|
||||
\and
|
||||
\cnttest{\value{Agda@Current} - #1}{>=}{
|
||||
\value{Agda@AlignStart}}
|
||||
\)}{\AgdaIndentSpace{}}{}}
|
||||
|
||||
% Underscores are typeset using \AgdaUnderscore{}.
|
||||
\newcommand{\AgdaUnderscore}{\_}
|
||||
|
||||
\endinput
|
||||
1218
papers/scp/llncs.cls
Executable file
1218
papers/scp/llncs.cls
Executable file
File diff suppressed because it is too large
Load diff
BIN
papers/scp/llncs2e/fig1.eps
Executable file
BIN
papers/scp/llncs2e/fig1.eps
Executable file
Binary file not shown.
139
papers/scp/llncs2e/history.txt
Executable file
139
papers/scp/llncs2e/history.txt
Executable file
|
|
@ -0,0 +1,139 @@
|
|||
Version history for the LLNCS LaTeX2e class
|
||||
|
||||
date filename version action/reason/acknowledgements
|
||||
----------------------------------------------------------------------------
|
||||
29.5.96 letter.txt beta naming problems (subject index file)
|
||||
thanks to Dr. Martin Held, Salzburg, AT
|
||||
|
||||
subjindx.ind renamed to subjidx.ind as required
|
||||
by llncs.dem
|
||||
|
||||
history.txt introducing this file
|
||||
|
||||
30.5.96 llncs.cls incompatibility with new article.cls of
|
||||
1995/12/20 v1.3q Standard LaTeX document class,
|
||||
\if@openbib is no longer defined,
|
||||
reported by Ralf Heckmann and Graham Gough
|
||||
solution by David Carlisle
|
||||
|
||||
10.6.96 llncs.cls problems with fragile commands in \author field
|
||||
reported by Michael Gschwind, TU Wien
|
||||
|
||||
25.7.96 llncs.cls revision a corrects:
|
||||
wrong size of text area, floats not \small,
|
||||
some LaTeX generated texts
|
||||
reported by Michael Sperber, Uni Tuebingen
|
||||
|
||||
16.4.97 all files 2.1 leaving beta state,
|
||||
raising version counter to 2.1
|
||||
|
||||
8.6.97 llncs.cls 2.1a revision a corrects:
|
||||
unbreakable citation lists, reported by
|
||||
Sergio Antoy of Portland State University
|
||||
|
||||
11.12.97 llncs.cls 2.2 "general" headings centered; two new elements
|
||||
for the article header: \email and \homedir;
|
||||
complete revision of special environments:
|
||||
\newtheorem replaced with \spnewtheorem,
|
||||
introduced the theopargself environment;
|
||||
two column parts made with multicol package;
|
||||
add ons to work with the hyperref package
|
||||
|
||||
07.01.98 llncs.cls 2.2 changed \email to simply switch to \tt
|
||||
|
||||
25.03.98 llncs.cls 2.3 new class option "oribibl" to suppress
|
||||
changes to the thebibliograpy environment
|
||||
and retain pure LaTeX codes - useful
|
||||
for most BibTeX applications
|
||||
|
||||
16.04.98 llncs.cls 2.3 if option "oribibl" is given, extend the
|
||||
thebibliograpy hook with "\small", suggested
|
||||
by Clemens Ballarin, University of Cambridge
|
||||
|
||||
20.11.98 llncs.cls 2.4 pagestyle "titlepage" - useful for
|
||||
compilation of whole LNCS volumes
|
||||
|
||||
12.01.99 llncs.cls 2.5 counters of orthogonal numbered special
|
||||
environments are reset each new contribution
|
||||
|
||||
27.04.99 llncs.cls 2.6 new command \thisbottomragged for the
|
||||
actual page; indention of the footnote
|
||||
made variable with \fnindent (default 1em);
|
||||
new command \url that copys its argument
|
||||
|
||||
2.03.00 llncs.cls 2.7 \figurename and \tablename made compatible
|
||||
to babel, suggested by Jo Hereth, TU Darmstadt;
|
||||
definition of \url moved \AtBeginDocument
|
||||
(allows for url package of Donald Arseneau),
|
||||
suggested by Manfred Hauswirth, TU of Vienna;
|
||||
\large for part entries in the TOC
|
||||
|
||||
16.04.00 llncs.cls 2.8 new option "orivec" to preserve the original
|
||||
vector definition, read "arrow" accent
|
||||
|
||||
17.01.01 llncs.cls 2.9 hardwired texts made polyglot,
|
||||
available languages: english (default),
|
||||
french, german - all are "babel-proof"
|
||||
|
||||
20.06.01 splncs.bst public release of a BibTeX style for LNCS,
|
||||
nobly provided by Jason Noble
|
||||
|
||||
14.08.01 llncs.cls 2.10 TOC: authors flushleft,
|
||||
entries without hyphenation; suggested
|
||||
by Wiro Niessen, Imaging Center - Utrecht
|
||||
|
||||
23.01.02 llncs.cls 2.11 fixed footnote number confusion with
|
||||
\thanks, numbered institutes, and normal
|
||||
footnote entries; error reported by
|
||||
Saverio Cittadini, Istituto Tecnico
|
||||
Industriale "Tito Sarrocchi" - Siena
|
||||
|
||||
28.01.02 llncs.cls 2.12 fixed footnote fix; error reported by
|
||||
Chris Mesterharm, CS Dept. Rutgers - NJ
|
||||
|
||||
28.01.02 llncs.cls 2.13 fixed the fix (programmer needs vacation)
|
||||
|
||||
17.08.04 llncs.cls 2.14 TOC: authors indented, smart \and handling
|
||||
for the TOC suggested by Thomas Gabel
|
||||
University of Osnabrueck
|
||||
|
||||
07.03.06 splncs.bst fix for BibTeX entries without year; patch
|
||||
provided by Jerry James, Utah State University
|
||||
|
||||
14.06.06 splncs_srt.bst a sorting BibTeX style for LNCS, feature
|
||||
provided by Tobias Heindel, FMI Uni-Stuttgart
|
||||
|
||||
16.10.06 llncs.dem 2.3 removed affiliations from \tocauthor demo
|
||||
|
||||
11.12.07 llncs.doc note on online visibility of given e-mail address
|
||||
|
||||
15.06.09 splncs03.bst new BibTeX style compliant with the current
|
||||
requirements, provided by Maurizio "Titto"
|
||||
Patrignani of Universita' Roma Tre
|
||||
|
||||
30.03.10 llncs.cls 2.15 fixed broken hyperref interoperability;
|
||||
patch provided by Sven Koehler,
|
||||
Hamburg University of Technology
|
||||
|
||||
15.04.10 llncs.cls 2.16 fixed hyperref warning for informatory TOC entries;
|
||||
introduced \keywords command - finally;
|
||||
blank removed from \keywordname, flaw reported
|
||||
by Armin B. Wagner, IGW TU Vienna
|
||||
|
||||
15.04.10 llncs.cls 2.17 fixed missing switch "openright" used by \backmatter;
|
||||
flaw reported by Tobias Pape, University of Potsdam
|
||||
|
||||
27.09.13 llncs.cls 2.18 fixed "ngerman" incompatibility; solution provided
|
||||
by Bastian Pfleging, University of Stuttgart
|
||||
|
||||
04.09.17 llncs.cls 2.19 introduced \orcidID command
|
||||
|
||||
10.03.18 llncs.cls 2.20 adjusted \doi according to CrossRef requirements;
|
||||
TOC: removed affiliation numbers
|
||||
|
||||
splncs04.bst added doi field;
|
||||
bold journal numbers
|
||||
|
||||
samplepaper.tex new sample paper
|
||||
|
||||
llncsdoc.pdf new LaTeX class documentation
|
||||
1218
papers/scp/llncs2e/llncs.cls
Executable file
1218
papers/scp/llncs2e/llncs.cls
Executable file
File diff suppressed because it is too large
Load diff
BIN
papers/scp/llncs2e/llncsdoc.pdf
Executable file
BIN
papers/scp/llncs2e/llncsdoc.pdf
Executable file
Binary file not shown.
19
papers/scp/llncs2e/readme.txt
Executable file
19
papers/scp/llncs2e/readme.txt
Executable file
|
|
@ -0,0 +1,19 @@
|
|||
Dear LLNCS user,
|
||||
|
||||
The files in this directory belong to the LaTeX2e package for
|
||||
Lecture Notes in Computer Science (LNCS) of Springer-Verlag.
|
||||
|
||||
It consists of the following files:
|
||||
|
||||
readme.txt this file
|
||||
|
||||
history.txt the version history of the package
|
||||
|
||||
llncs.cls the LaTeX2e document class
|
||||
|
||||
samplepaper.tex a sample paper
|
||||
fig1.eps a figure used in the sample paper
|
||||
|
||||
llncsdoc.pdf the documentation of the class (PDF version)
|
||||
|
||||
splncs04.bst current LNCS BibTeX style with alphabetic sorting
|
||||
BIN
papers/scp/llncs2e/samplepaper.pdf
Normal file
BIN
papers/scp/llncs2e/samplepaper.pdf
Normal file
Binary file not shown.
150
papers/scp/llncs2e/samplepaper.tex
Executable file
150
papers/scp/llncs2e/samplepaper.tex
Executable file
|
|
@ -0,0 +1,150 @@
|
|||
% This is samplepaper.tex, a sample chapter demonstrating the
|
||||
% LLNCS macro package for Springer Computer Science proceedings;
|
||||
% Version 2.20 of 2017/10/04
|
||||
%
|
||||
\documentclass[runningheads]{llncs}
|
||||
%
|
||||
\usepackage{graphicx}
|
||||
% Used for displaying a sample figure. If possible, figure files should
|
||||
% be included in EPS format.
|
||||
%
|
||||
% If you use the hyperref package, please uncomment the following line
|
||||
% to display URLs in blue roman font according to Springer's eBook style:
|
||||
% \renewcommand\UrlFont{\color{blue}\rmfamily}
|
||||
|
||||
\begin{document}
|
||||
%
|
||||
\title{Contribution Title\thanks{Supported by organization x.}}
|
||||
%
|
||||
%\titlerunning{Abbreviated paper title}
|
||||
% If the paper title is too long for the running head, you can set
|
||||
% an abbreviated paper title here
|
||||
%
|
||||
\author{First Author\inst{1}\orcidID{0000-1111-2222-3333} \and
|
||||
Second Author\inst{2,3}\orcidID{1111-2222-3333-4444} \and
|
||||
Third Author\inst{3}\orcidID{2222--3333-4444-5555}}
|
||||
%
|
||||
\authorrunning{F. Author et al.}
|
||||
% First names are abbreviated in the running head.
|
||||
% If there are more than two authors, 'et al.' is used.
|
||||
%
|
||||
\institute{Princeton University, Princeton NJ 08544, USA \and
|
||||
Springer Heidelberg, Tiergartenstr. 17, 69121 Heidelberg, Germany
|
||||
\email{lncs@springer.com}\\
|
||||
\url{http://www.springer.com/gp/computer-science/lncs} \and
|
||||
ABC Institute, Rupert-Karls-University Heidelberg, Heidelberg, Germany\\
|
||||
\email{\{abc,lncs\}@uni-heidelberg.de}}
|
||||
%
|
||||
\maketitle % typeset the header of the contribution
|
||||
%
|
||||
\begin{abstract}
|
||||
The abstract should briefly summarize the contents of the paper in
|
||||
150--250 words.
|
||||
|
||||
\keywords{First keyword \and Second keyword \and Another keyword.}
|
||||
\end{abstract}
|
||||
%
|
||||
%
|
||||
%
|
||||
\section{First Section}
|
||||
\subsection{A Subsection Sample}
|
||||
Please note that the first paragraph of a section or subsection is
|
||||
not indented. The first paragraph that follows a table, figure,
|
||||
equation etc. does not need an indent, either.
|
||||
|
||||
Subsequent paragraphs, however, are indented.
|
||||
|
||||
\subsubsection{Sample Heading (Third Level)} Only two levels of
|
||||
headings should be numbered. Lower level headings remain unnumbered;
|
||||
they are formatted as run-in headings.
|
||||
|
||||
\paragraph{Sample Heading (Fourth Level)}
|
||||
The contribution should contain no more than four levels of
|
||||
headings. Table~\ref{tab1} gives a summary of all heading levels.
|
||||
|
||||
\begin{table}
|
||||
\caption{Table captions should be placed above the
|
||||
tables.}\label{tab1}
|
||||
\begin{tabular}{|l|l|l|}
|
||||
\hline
|
||||
Heading level & Example & Font size and style\\
|
||||
\hline
|
||||
Title (centered) & {\Large\bfseries Lecture Notes} & 14 point, bold\\
|
||||
1st-level heading & {\large\bfseries 1 Introduction} & 12 point, bold\\
|
||||
2nd-level heading & {\bfseries 2.1 Printing Area} & 10 point, bold\\
|
||||
3rd-level heading & {\bfseries Run-in Heading in Bold.} Text follows & 10 point, bold\\
|
||||
4th-level heading & {\itshape Lowest Level Heading.} Text follows & 10 point, italic\\
|
||||
\hline
|
||||
\end{tabular}
|
||||
\end{table}
|
||||
|
||||
|
||||
\noindent Displayed equations are centered and set on a separate
|
||||
line.
|
||||
\begin{equation}
|
||||
x + y = z
|
||||
\end{equation}
|
||||
Please try to avoid rasterized images for line-art diagrams and
|
||||
schemas. Whenever possible, use vector graphics instead (see
|
||||
Fig.~\ref{fig1}).
|
||||
|
||||
\begin{figure}
|
||||
\includegraphics[width=\textwidth]{fig1.eps}
|
||||
\caption{A figure caption is always placed below the illustration.
|
||||
Please note that short captions are centered, while long ones are
|
||||
justified by the macro package automatically.} \label{fig1}
|
||||
\end{figure}
|
||||
|
||||
\begin{theorem}
|
||||
This is a sample theorem. The run-in heading is set in bold, while
|
||||
the following text appears in italics. Definitions, lemmas,
|
||||
propositions, and corollaries are styled the same way.
|
||||
\end{theorem}
|
||||
%
|
||||
% the environments 'definition', 'lemma', 'proposition', 'corollary',
|
||||
% 'remark', and 'example' are defined in the LLNCS documentclass as well.
|
||||
%
|
||||
\begin{proof}
|
||||
Proofs, examples, and remarks have the initial word in italics,
|
||||
while the following text appears in normal font.
|
||||
\end{proof}
|
||||
For citations of references, we prefer the use of square brackets
|
||||
and consecutive numbers. Citations using labels or the author/year
|
||||
convention are also acceptable. The following bibliography provides
|
||||
a sample reference list with entries for journal
|
||||
articles~\cite{ref_article1}, an LNCS chapter~\cite{ref_lncs1}, a
|
||||
book~\cite{ref_book1}, proceedings without editors~\cite{ref_proc1},
|
||||
and a homepage~\cite{ref_url1}. Multiple citations are grouped
|
||||
\cite{ref_article1,ref_lncs1,ref_book1},
|
||||
\cite{ref_article1,ref_book1,ref_proc1,ref_url1}.
|
||||
%
|
||||
% ---- Bibliography ----
|
||||
%
|
||||
% BibTeX users should specify bibliography style 'splncs04'.
|
||||
% References will then be sorted and formatted in the correct style.
|
||||
%
|
||||
% \bibliographystyle{splncs04}
|
||||
% \bibliography{mybibliography}
|
||||
%
|
||||
\begin{thebibliography}{8}
|
||||
\bibitem{ref_article1}
|
||||
Author, F.: Article title. Journal \textbf{2}(5), 99--110 (2016)
|
||||
|
||||
\bibitem{ref_lncs1}
|
||||
Author, F., Author, S.: Title of a proceedings paper. In: Editor,
|
||||
F., Editor, S. (eds.) CONFERENCE 2016, LNCS, vol. 9999, pp. 1--13.
|
||||
Springer, Heidelberg (2016). \doi{10.10007/1234567890}
|
||||
|
||||
\bibitem{ref_book1}
|
||||
Author, F., Author, S., Author, T.: Book title. 2nd edn. Publisher,
|
||||
Location (1999)
|
||||
|
||||
\bibitem{ref_proc1}
|
||||
Author, A.-B.: Contribution title. In: 9th International Proceedings
|
||||
on Proceedings, pp. 1--2. Publisher, Location (2010)
|
||||
|
||||
\bibitem{ref_url1}
|
||||
LNCS Homepage, \url{http://www.springer.com/lncs}. Last accessed 4
|
||||
Oct 2017
|
||||
\end{thebibliography}
|
||||
\end{document}
|
||||
1548
papers/scp/llncs2e/splncs04.bst
Executable file
1548
papers/scp/llncs2e/splncs04.bst
Executable file
File diff suppressed because it is too large
Load diff
35
papers/scp/query.lagda
Normal file
35
papers/scp/query.lagda
Normal file
|
|
@ -0,0 +1,35 @@
|
|||
Everyone on this list will be familiar with Progress and Preservation
|
||||
for terms in a typed calculus. Write ∅ ⊢ M : A to indicate that term
|
||||
M has type A for closed M.
|
||||
|
||||
Progress. If ∅ ⊢ M : A then either M is a value or M —→ N,
|
||||
for some term N.
|
||||
|
||||
Preservation. If ∅ ⊢ M : A and M —→ N then ∅ ⊢ N : A.
|
||||
|
||||
It is easy to combine these two proofs into an evaluator.
|
||||
Write —↠ for the transitive and reflexive closure of —→.
|
||||
|
||||
Evaluation. If ∅ ⊢ M : A, then for every natural number n,
|
||||
either M —↠ V, where V is a value and the reduction sequence
|
||||
has no more than n steps, or M —↠ N, where N is not a value
|
||||
and the reduction sequence has n steps.
|
||||
|
||||
Evaluation implies that either M —↠ V or there is an infinite
|
||||
sequence M —→ M₁ —→ M₂ —→ ... that never reduces to a value;
|
||||
but this last result is not constructive, as deciding which of
|
||||
the two results holds is not decidable.
|
||||
|
||||
An Agda implementation of Evaluation provides an evaluator for terms:
|
||||
given a number n it will perform up to n steps of evaluation, stopping
|
||||
early if a value is reached. This is entirely obvious (at least in
|
||||
retrospect), but I have not seen it written down anywhere. For
|
||||
instance, this approach is not exploited in Software Foundations to
|
||||
evaluate terms (other methods are used instead). I have used it
|
||||
in my draft textbook:
|
||||
|
||||
https:plfa.inf.ed.ac.uk
|
||||
|
||||
Questions: What sources in the literature should one cite for this
|
||||
technique? How well-known is it as folklore?
|
||||
|
||||
245
papers/scp/reviews.txt
Normal file
245
papers/scp/reviews.txt
Normal file
|
|
@ -0,0 +1,245 @@
|
|||
|
||||
|
||||
|
||||
Dear Philip,
|
||||
|
||||
Thank you very much for having submitted to SBMF 2018.
|
||||
|
||||
We are glad to inform you that the paper "Programming Language
|
||||
Foundations in Agda" has been accepted for presentation and inclusion
|
||||
in the LNCS proceedings of SBMF 2018.
|
||||
|
||||
We have received 30 submissions to this edition of the conference,
|
||||
accepting 14 submissions among them; each submission received a
|
||||
minimum of three and a maximum of five review reports. Once again
|
||||
congratulations for being among a select few!
|
||||
|
||||
We enclose below the review reports of your submission, provided by
|
||||
our international program committee. Please consider them carefully
|
||||
when preparing your camera-ready paper.
|
||||
|
||||
Please note that the camera-ready paper is due on September 11th, and
|
||||
the deadline is strict. You will be invited to submit your final
|
||||
manuscript via the EasyChair system. Please make sure that you use the
|
||||
LNCS style file (without any manual modifications) for preparing the
|
||||
camera-ready version and also include a signed copy of the LNCS
|
||||
copyright form in your camera-ready submission.
|
||||
|
||||
Thank you very much again for having submitted your paper, and we are
|
||||
looking forward to meeting you and listening to you at SBMF 2018.
|
||||
|
||||
Best regards -- Tiago Massoni and Mohammad Mousavi
|
||||
|
||||
PC Chairs of SBMF 2018
|
||||
|
||||
|
||||
----------------------- REVIEW 1 ---------------------
|
||||
PAPER: 14
|
||||
TITLE: Programming Language Foundations in Agda
|
||||
AUTHORS: Philip Wadler
|
||||
|
||||
Overall evaluation: 3 (strong accept)
|
||||
|
||||
----------- Overall evaluation -----------
|
||||
This paper is an experience report about using the proof assistant
|
||||
Agda to teach some basic topics in programming language theory,
|
||||
following the lines of the book Software Foundations (SF) which uses
|
||||
Coq. The Agda development discussed in the paper is part of a larger
|
||||
development comprising a new textbook that uses Agda and covers some
|
||||
of the topics of SF. There are three main contributions as I see
|
||||
them. First, Agda is compared with Coq for suitability of teaching
|
||||
this sort of material. Second, the paper spells out how constructive
|
||||
proofs of progress and subject reduction can be composed in a simple
|
||||
way to define an evaluator. Third, some arguments are given in favor
|
||||
of using an inherently-typed representation of terms rather than raw
|
||||
terms.
|
||||
|
||||
The comparison with Agda and Coq has no surprises for experts, but is
|
||||
clearly written and should serve as a valuable guide to educators.
|
||||
Key aspects of the two systems are explained, from the point of view
|
||||
of teaching core PL concepts at an introductory level, and the paper
|
||||
is likely to make a broad community aware of the newly developed
|
||||
alternative to SF. The comparisons are interesting points, phrased
|
||||
fairly and succinctly, and are based on substantial teaching
|
||||
experience.
|
||||
|
||||
The direct use of progress plus subject reduction as the components of
|
||||
an evaluator seems so obvious that it is surprising that, as the
|
||||
author explains, it does not seem to be very widely known (and not
|
||||
previously published). This part of the paper therefore provides
|
||||
novel scientific content.
|
||||
|
||||
The discussion of inherently-typed term representation, and de Bruin
|
||||
notation, is somewhat high level, less clear and less accessible to
|
||||
non-experts than the other topics, but still interesting.
|
||||
|
||||
Details
|
||||
|
||||
The writing is excellent and I have only a few minor issues to point
|
||||
out.
|
||||
|
||||
Given that the author aims to improve on SF, not merely reproduce it
|
||||
in Agda, I suggest not settling for progress and preservation, but
|
||||
also include some semantic type soundness result. The significance of
|
||||
such results is well argued in Dreyer's invited talk at POPL 2018.
|
||||
|
||||
Perhaps the biggest contribution of the work reported here is the
|
||||
possibility to do empirical studies of learning with two different
|
||||
forms of interactive proving, as remarked near the top of page 11. I
|
||||
encourage the author to pursue that.
|
||||
|
||||
|
||||
- The first line of the abstract refers to SF as "the leading textbook
|
||||
for formal methods". If there is evidence for that, it should be
|
||||
mentioned in the paper; otherwise it should be watered down. Formal
|
||||
methods is a broader field than the topics covered in SF, and SF is
|
||||
not the only widely used textbook on those topics or others in
|
||||
formal methods. [done]
|
||||
|
||||
- page 2 "Pierce and Benjamin" should be just Pierce [done]
|
||||
|
||||
- page 6 the first term in Fig 1 uses dot for application, which is
|
||||
sufficiently nonstandard to deserve mention by the time the figure
|
||||
is discussed; it doesn't become obvious until fig 2
|
||||
|
||||
- fig 2 could benefit with a bit more explanation of the formal
|
||||
notation, for readers (like this reviewer) not familiar with Agda.
|
||||
For example, on first glance it's surprising to see the identifier
|
||||
progress re-defined, and back-tick empty-parens isn't obviously the
|
||||
variable case. [done]
|
||||
|
||||
- page 13 comments about formatting, "All of the example ... output."
|
||||
are not so interesting and could be omitted. [disagree]
|
||||
|
||||
- section 5 please consider showing some notation and explaining
|
||||
inherently-typed terms in more detail
|
||||
|
||||
- page 13 "any proofs that appear in one..." is ambiguous. It could
|
||||
refer to results that are only relevant to one but not the other, in
|
||||
which case stripping them out could be an unfair comparison.
|
||||
Perhaps you mean results that simply happen not to be stated and
|
||||
proved in one of the two developments. [done]
|
||||
|
||||
|
||||
----------------------- REVIEW 2 ---------------------
|
||||
PAPER: 14
|
||||
TITLE: Programming Language Foundations in Agda
|
||||
AUTHORS: Philip Wadler
|
||||
|
||||
Overall evaluation: 2 (accept)
|
||||
|
||||
----------- Overall evaluation -----------
|
||||
This paper reports an alternative to the Software Foundations book
|
||||
(SF) by Pierce et al. The author claims that the language Agda is a
|
||||
better vehicle to teaching the foundations of programming languages in
|
||||
comparison to Coq. According to his experience using SF, much of the
|
||||
learning effort goes to tactics. His textbook, Programming Language
|
||||
Foundations in Agda, also provides an elegant way to get from
|
||||
constructive proofs of preservation and progress to a prototype
|
||||
evaluator.
|
||||
|
||||
As part of the "Experience reports regarding teaching formal methods"
|
||||
of our Call for Paper, I think this work will introduce to the
|
||||
audience a relevant alterantive to SF and an important new way to
|
||||
teaching formal methods and programming languages.
|
||||
|
||||
|
||||
----------------------- REVIEW 3 ---------------------
|
||||
PAPER: 14
|
||||
TITLE: Programming Language Foundations in Agda
|
||||
AUTHORS: Philip Wadler
|
||||
|
||||
Overall evaluation: 2 (accept)
|
||||
|
||||
----------- Overall evaluation -----------
|
||||
In this paper the author presents his personal experience on writing a
|
||||
textbook covering the same material as the famous “Software
|
||||
Foundations” in Agda instead of Coq. The main motivation to use Agda
|
||||
is pedagogical. For understanding a Coq proof a student will typically
|
||||
need to run the proof in an interactive prover. However, it should be
|
||||
possible for a student to read an Agda proof without running it in a
|
||||
prover. For the modest size proofs that the textbook uses the lengths
|
||||
of the proofs are quite comparable. The author has given some
|
||||
comparisons between the the two textbooks in Section 3. Sections 4 and
|
||||
5 present some of the decisions that the author has made in writing
|
||||
the book (prototype evaluator and inherent typing). The paper in
|
||||
general is a pleasant read and the comparisons between the books are
|
||||
interesting. I tend to agree with Nate Foster that it is certainly
|
||||
interesting to empirically evaluate the reluctance of the students to
|
||||
use theorem provers. Such an evaluation can quite a strong case for
|
||||
writing the new book.
|
||||
|
||||
-------------------------------------------------------
|
||||
|
||||
Paper: 14
|
||||
Authors: Philip Wadler
|
||||
Title: Programming Language Foundations in Agda
|
||||
|
||||
-------------------------------------------------------
|
||||
|
||||
Dear Philip,
|
||||
|
||||
You have already received the comments by the reviewers in a
|
||||
previous email. Please take them carefully into account when
|
||||
preparing your camera-ready paper for the proceedings. The final
|
||||
paper and the signed copyright form are due on
|
||||
|
||||
September 11, 2018
|
||||
|
||||
This is a firm deadline for the production of the proceedings.
|
||||
You should submit your paper using your EasyChair proceedings
|
||||
author role for SBMF 2018.
|
||||
|
||||
1. FINAL PAPER: Please submit the files belonging to your
|
||||
camera-ready paper using your EasyChair author account. Follow
|
||||
the instructions after the login for uploading two files:
|
||||
|
||||
(1) either a zipped file containing all your LaTeX sources or
|
||||
a Word file in the RTF format, and
|
||||
|
||||
(2) the PDF version of your camera-ready paper
|
||||
|
||||
Please follow strictly
|
||||
the author instructions of Springer-Verlag when preparing the
|
||||
final version:
|
||||
|
||||
http://www.springer.de/comp/lncs/authors.html
|
||||
|
||||
Our publisher has recently introduced an extra control loop: once
|
||||
data processing is finished, they will contact all corresponding
|
||||
authors and ask them to check their papers. We expect this to
|
||||
happen shortly before the printing of the proceedings. At that
|
||||
time your quick interaction with Springer-Verlag will be greatly
|
||||
appreciated.
|
||||
|
||||
2. COPYRIGHT: Please upload a signed and completed copyright form
|
||||
to us as soon as possible. The Springer copyright forms can be
|
||||
found at
|
||||
|
||||
https://resource-cms.springernature.com/springer-cms/rest/v1/content/15433008/data/Contract_Book_Contributor_Consent_to_Publish_LNCS_SIP
|
||||
|
||||
|
||||
It is sufficient for one of the authors to sign the copyright
|
||||
form. You can scan the form into PDF or any other standard image
|
||||
format.
|
||||
|
||||
We greatly appreciate your cooperation in these matters. Thank
|
||||
you again for your contribution to SBMF 2018.
|
||||
|
||||
All questions about papers should be sent to the volume editors
|
||||
Tiago Massoni <massoni@computacao.ufcg.edu.br> and
|
||||
Mohammadreza Mousavi <mm789@leicester.ac.uk>.
|
||||
|
||||
Sincerely,
|
||||
-- Tiago Massoni and
|
||||
Mohammad Mousavi
|
||||
|
||||
|
||||
|
||||
|
||||
The LNCS edition will allow papers to present up to two (2) extra
|
||||
pages in their final version, so you may use this to better
|
||||
accommodate changes required by the reviews.
|
||||
|
||||
Regards,
|
||||
Tiago and Mohammad.
|
||||
1508
papers/scp/splncsnat.bst
Normal file
1508
papers/scp/splncsnat.bst
Normal file
File diff suppressed because it is too large
Load diff
20
papers/scp/text.lagda
Normal file
20
papers/scp/text.lagda
Normal file
|
|
@ -0,0 +1,20 @@
|
|||
\documentclass{article}
|
||||
\usepackage{bbm}
|
||||
\usepackage[greek,english]{babel}
|
||||
\usepackage{ucs}
|
||||
\usepackage[utf8x]{inputenc}
|
||||
\usepackage{autofe}
|
||||
\usepackage{agda}
|
||||
\begin{document}
|
||||
|
||||
\begin{code}
|
||||
data αβγδεζθικλμνξρστυφχψω : Set₁ where
|
||||
|
||||
postulate
|
||||
→⇒⇛⇉⇄↦⇨↠⇀⇁ : Set
|
||||
\end{code}
|
||||
|
||||
\[
|
||||
∀X [ ∅ ∉ X ⇒ ∃f:X ⟶ ⋃ X\ ∀A ∈ X (f(A) ∈ A) ]
|
||||
\]
|
||||
\end{document}
|
||||
BIN
sbmf/.DS_Store
vendored
BIN
sbmf/.DS_Store
vendored
Binary file not shown.
Loading…
Reference in a new issue