Projects per year
Abstract / Description of output
One of the leading textbooks for formal methods is 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, 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 inherentlytyped 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
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 inherentlytyped 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 language  English 

Title of host publication  Formal Methods: Foundations and Applications 
Subtitle of host publication  21st Brazilian Symposium, SBMF 2018, Salvador, Brazil, November 26 — November 30, 2018, Proceedings 
Place of Publication  Salvador, Brazil 
Publisher  Springer, Cham 
Pages  5673 
Number of pages  18 
ISBN (Electronic)  9783030030445 
ISBN (Print)  9783030030438 
DOIs  
Publication status  Published  2018 
Event  XXI SBMF Brazilian Symposium on Formal Methods (SBMF)  Salvador, Brazil Duration: 26 Nov 2018 → 30 Nov 2018 http://www.sbmf2018.ufba.br/ 
Publication series
Name  Lecture Notes in Computer Science 

Publisher  Springer, Cham 
Volume  11254 
ISSN (Print)  03029743 
ISSN (Electronic)  16113349 
Name  Programming and Software Engineering 

Volume  11254 
Symposium
Symposium  XXI SBMF Brazilian Symposium on Formal Methods (SBMF) 

Country/Territory  Brazil 
City  Salvador 
Period  26/11/18 → 30/11/18 
Internet address 
Fingerprint
Dive into the research topics of 'Programming Language Foundations in Agda'. Together they form a unique fingerprint.Projects
 1 Finished

From Data Types to Session Types  A Basis for Concurrency and Distribution
20/05/13 → 19/11/20
Project: Research
Research output
 1 Book

Programming Language Foundations in Agda
Wadler, P. & Kokke, W., 2018Research output: Book/Report › Book
Open Access