Use of a proof assistant in teaching provides immediate feedback to students. Proof assistants permit formal statements of propositions and proofs in a way that can be checked by a computer. After five years using the leading textbook Software Foundations in the classroom, which is based on the proof assistant Coq, I have come to the conclusion that Coq is not the best vehicle for this purpose. Accordingly, I have written a new textbook, Programming Language Foundations in Agda (PLFA), based on the proof assistant Agda. In this talk I will describe three interesting findings that I learned from writing PFLA.
The textbook is written as a literate Agda script, and can be found here: http://plfa.inf.ed.ac.uk
Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh and Senior Research Fellow at IOHK. He is an ACM Fellow, a Fellow of the Royal Society of Edinburgh, and editor-in-chief of Proceedings of the ACM for Programming Languages. He is past chair of ACM SIGPLAN, past holder of a Royal Society-Wolfson Research Merit Fellowship, winner of the SIGPLAN Distinguished Service Award, and a winner of the POPL Most Influential Paper Award. Previously, he worked or studied at Stanford, Xerox Parc, CMU, Oxford, Chalmers, Glasgow, Bell Labs, and Avaya Labs, and visited as a guest professor in Copenhagen, Sydney, and Paris. He has an h-index of 66 with more than 24,000 citations to his work, according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004), Generics and Collections in Java (O'Reilly, 2006), and Programming Language Foundations in Agda (2018). He has delivered invited talks in locations ranging from Aizu to Zurich.
More infos are available here: