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 book also has two readings. It may be parsed as “(Programming Language) Foundations in Agda” or “Programming (Language Foundations) in Agda” — the specifications we will write in the proof assistant Agda both describe programming languages and are themselves programmes.

The book 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. 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 misapprehensions.

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.

Personal remarks

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 Benjamin Pierce’s excellent TAPL. My version was based of Pierce’s subsequent textbook, Software Foundations, written in collaboration with others and based on Coq. I am convinced of Pierce’s claim that basing a course around a proof assistant aids learning, as summarised in his ICFP Keynote, Lambda, The Ultimate TA.

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 notation construct permits pleasingly flexible syntax, it can be confusing that the same concept must always be given two names, e.g., both subst N x M and N [x := M]. Names of tactics are sometimes short and sometimes long; naming conventions in the standard library can be wildly inconsistent. Propositions as types as a foundation of proof is present but hidden.

I found myself keen to recast the course in Agda. 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 _[_:=_]. The standard library is not perfect, but there is a fair attempt at consistency. Propositions as types as a foundation of proof is on proud display.

Alas, there is no textbook for programming language theory in Agda. Stump’s Verified Functional Programming in Agda 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 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 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.

Most of the text was written during a sabbatical in the first half of 2018.

— Philip Wadler, Rio de Janeiro, January–June 2018

A word on the exercises

Exercises labelled “(recommended)” are the ones students are required to do in the class taught at Edinburgh from this textbook.

Exercises labelled “(stretch)” are there to provide an extra challenge. Few students do all of these, but most attempt at least a few.

Exercises labelled “(practice)” are included for those who want extra practice.

You may answer the exercises by downloading the book from github and editing where it says “– Your code goes here”. Alternatively, you may be given a file to edit containing exercises for a given coursework.

In either case, you may need to import additional library functions required for the solution. You may also need to set up PLFA as an Agda library, as described in Getting Started.

Please do not post answers to the exercises in a public place.

There is a private repository of answers to selected questions on github. Please contact Philip Wadler if you would like to access it.