michael/csci8980-f21
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Cleaned up SCP source.

Browse source
This commit is contained in:
Wen Kokke 2019-07-01 17:53:50 +02:00
parent 85f0dce1ac
commit 5d21b09743
16 changed files with 0 additions and 4757 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
papers/scp/PLFA.pdf
View file

Binary file not shown.

32
papers/scp/extra.lagda
View file

@ -1,32 +0,0 @@
\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/final.zip
View file

Binary file not shown.

660
papers/scp/latex/PLFA.tex
View file

@ -1,660 +0,0 @@
%\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
View file

@ -1,691 +0,0 @@
% ----------------------------------------------------------------------
% 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/llncs2e/fig1.eps
View file

Binary file not shown.

139
papers/scp/llncs2e/history.txt
View file

@ -1,139 +0,0 @@
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
View file

File diff suppressed because it is too large Load diff

BIN
papers/scp/llncs2e/llncsdoc.pdf
View file

Binary file not shown.

19
papers/scp/llncs2e/readme.txt
View file

@ -1,19 +0,0 @@
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
View file

Binary file not shown.

150
papers/scp/llncs2e/samplepaper.tex
View file

@ -1,150 +0,0 @@
% 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
View file

File diff suppressed because it is too large Load diff

35
papers/scp/query.lagda
View file

@ -1,35 +0,0 @@
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
View file

@ -1,245 +0,0 @@
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.

20
papers/scp/text.lagda
View file

@ -1,20 +0,0 @@
\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}