Programming Language Foundations in Agda

Kerewin Kokke, Jeremy G. Siek, Philip Wadler

Research output: Contribution to journalArticlepeer-review

Abstract

One of the leading textbooks for formal methods is Software Foundations (SF), written by Benjamin Pierce in collaboration with others, and based onCoq. After five years using SF in the classroom, we came 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, we have written a new textbook, Programming Language Foundations in Agda (PLFA). PLFA covers much of the same ground as SF, although it is not a slavish imitation.

What did we 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 we find it in the literature. Third, that using extrinsically-typed terms is far less perspicuous than using intrinsically-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: http://plfa.inf.ed.ac.uk
Original languageEnglish
Article number102440
Pages (from-to)1-15
Number of pages15
JournalScience of Computer Programming
Volume194
Early online date24 Mar 2020
DOIs
Publication statusPublished - 1 Aug 2020

Keywords

  • Agda
  • Coq
  • lambda calculus
  • dependent types

Fingerprint Dive into the research topics of 'Programming Language Foundations in Agda'. Together they form a unique fingerprint.

Cite this