7 Resources

\(\newcommand{\la}{\lambda} \newcommand{\Ga}{\Gamma} \newcommand{\ra}{\rightarrow} \newcommand{\Ra}{\Rightarrow} \newcommand{\La}{\Leftarrow} \newcommand{\tl}{\triangleleft} \newcommand{\ir}[3]{\displaystyle\frac{#2}{#3}~{\textstyle #1}}\)

"Honesty’s an actor’s worst mistake"
(That’s How I Escaped My Certain Fate, Mission of Burma, 1980)

With a few exceptions (such as historical background), you shouldn’t be looking at the following resources while you are working through this material, especially if you are doing so for academic credit. But there are lots of great references below that go into more depth about many of the topics here.

I can’t really recommend Wikipedia for either technical or cultural background. You will have better luck starting with the Stanford Encyclopedia of Philosophy. The SEP has articles written, reviewed, and edited by expert professionals.

Philip Wadler’s papers "Propositions as Types" and "Proofs are Programs" are very readable overviews of the ideas behind the Curry-Howard correspondence and their consequences (and his talks on the subject are very watchable, if you have the time).

The paper "The Road To Modern Logic - An Interpretation", by Jose Ferreiros (Bulletin of Symbolic Logic, 7:4, pp. 441-484, 2001) is a very detailed study of the historic development of first-order logic. It helped inform my decision to focus instead on higher-order logic.

The Coq and Agda Web pages are good starting points for learning more about these proof assistants. There are several good books using Coq, including the entirely online Software Foundations (SF). I have taught from Software Foundations several times. Many writers have contributed to it. Some of my prose is in it, and some which I originally wrote for it appears instead in the Proof Assistants chapter of LACI. Working through SF will teach you a lot both about Coq and about the broader context of operational semantics and type theory.

The Coq’Art book mentioned in section section 4.3.5 is "Interactive theorem proving and program development" by Yves Bertot and Pierre Castéran, which has the subtitle "Coq’Art: The Calculus of Inductive Constructions". It is older and somewhat out of date, but it is a good bottom-up introduction to Coq, from which I learned a lot.

Philip Wadler and Wen Kokke originally intended to produce an Agda translation of SF, but ended up writing a separate book, Programming Language Foundations in Agda (PLFA). I have also taught from this book, and it convinced me to switch from SF, and to emphasize Agda, rather than Coq, here. PLFA is much newer, less polished, and more of a work in progress, but I also recommend it for the same reasons I recommend SF.

The only other book on Agda of which I’m aware is Aaron Stump’s "Verified Functional Programming in Agda" (VFPA). If you liked the material on Kripke models in section section 2.9, you may be interested in VFPA’s thorough treatment of soundness and completeness in Agda. Be warned, though: the implementation of Braun heaps in the book mimics the conventional presentation too closely, and consequently does too much work. The code isn’t guaranteed to work with current versions of Agda.

The book I consulted the most in learning and preparing this material was "Lectures on the Curry-Howard isomorphism", by Morten Heine Sørensen and Pawel Urzyczyn. Besides being meticulous about inference rules, and building from the basics towards the most general systems, it presents a range of contextual material, including Heyting algebras, prover-skeptic dialogues, and a complete exposition of why Type:Type leads to contradiction. "Type theory and formal proof: an introduction" by Rob Nederpelt and Herman Geuvers is also careful about rules, including those for definitions.

Those two books are expensive. Simon Thompson has graciously made the earlier "Type theory and functional programming" available for free on his website.

Herman Geuvers offers a nice overview of Coq, Agda, and many other systems in his 2009 paper "Proof assistants: history, ideas, and future".

Idris is a programming language with Haskell-like syntax and full support for dependent types. Its designer, Edwin Brady, wants it to be used for programs that are actually run, not just compiled! There is now a book, "Type-driven development with Idris".

A recent development worth keeping an eye on is Lean, a state-of-the-art proof assistant created by Microsoft Research and CMU. The online tutorial is quite well written, and runs a version of the software compiled to Javascript in your browser, making it very easy to take a quick look (no manual installation required). Lean is fairly immature compared to Coq and Agda, and doesn’t have their stability yet.

David Turner, the designer of Miranda (the first practical lazy functional programming language, and a major inspiration for Haskell) has a nice paper titled "Total Functional Programming" which points out many drawbacks of the common practice of allowing partial functions, even for systems that are not being used for proof.

David Christiansen created a tutorial describing a more sophisticated approach (normalization by evaluation) to the same goal as Proust, namely writing a type checker in Racket for a small dependently-typed language. This tutorial is very accessible for those who have worked through LACI.

I originally developed Proust to help me understand what a proof assistant might be doing. Students would ask about some behaviour of Coq, and I couldn’t give them good explanations. There is nothing original in Proust; it’s a synthesis of ideas. In addition to the works listed above, I drew on the papers A tutorial implementation of a dependently typed lambda calculus by Loh, McBride, and Swierstra, and ΠΣ: Dependent types without the sugar by Altenkirch, Danielsson, Loh, and Oury, as well as blog posts by Andrej Bauer (explaining universes) and Lennart Augustsson (explaining sorts).

For careful exposition of the ideas behind holes, unification, and pattern matching, I relied on the PhD theses of Conor McBride, Lena Magnusson, and Ulf Norell. The survey (currently on arXiv) by Jana Dunfield and Neel Krishnaswami will tell you a lot about bidirectional typing, including choices in the "recipe" for defining rules; David Christiansen has a shorter introductory writeup.

7.1 Acknowledgements

I learned about Agda first from Peter Dybjer’s lectures at OPLSS 2015. Stephanie Weirich was and is an inspiration, and was very patient with my foolish early questions; her OPLSS 2014 lectures were quite helpful. David Darais and Wen Kokke answered foolish late questions as I prepared for my first full course in Agda, and Jacques Carette helped with some of the thornier Agda issues I encountered while expanding the Agda coverage in LACI.

I workshopped Proust to a few brave souls at the Recurse Center in NYC in October 2015, and used it in CS 245E at the University of Waterloo in Fall 2016, Spring 2017, and Fall 2020. Ifaz Kabir and Marianna Rapoport were excellent TAs. Student feedback helped a lot. Kai Rüsch found a subtle bug in an early version of Proust and, amusingly, used it to prove contradiction. Astra Kolomatskaia found several bugs and typos during her later preparation for using Proust with math students at SUNY Stonybrook in summer 2020; watching her lectures and discussing them suggested many small improvements to LACI. Astra and Mike Shulman had many good suggestions that improved the presentation of predicate logic. Talia McCormick came to office hours regularly and asked all the right questions. Some of the exposition in LACI was worked out on the whiteboard with her. John Clements gave me an early sign that non-students could also be enthusiastic about this approach.

The main reason this material is free for you to read is the direct and indirect support provided by the Governments of Canada and Ontario and their funding agencies, as well as the generous intellectual property policy of my employer, the University of Waterloo.

I wrote the first full version of LACI in the spring of 2020 while under COVID-19 lockdown, made infinitely more tolerable by the unflagging support and encouragement of my partner.

(Brooklyn, August 2020)