This course is in two parts, each three hours long.

Part I is an introduction to formal methods in Agda, covering datatypes, recursion, structural induction, indexed datatypes, dependent functions, and induction over evidence; with focus on formal definitions of naturals, addition, and inequality, and their properties.

Part II is an introduction to formal models of simply-typed lambda calculus in Agda, including reduction, type rules, and progress and preservation, and (as a consequence) evaluation of lambda terms. Part II depends on Part I, but Part I can be skipped by those already familiar with Agda.

The textbook is freely available online:

Programming Language Foundations in Agda

and on Github.

The books has been used for teaching by me at:

• University of Edinburgh (Sep-Dec 2018)
• Pontifical Catholic University of Rio de Janeiro (PUC-Rio) (Mar-Jul 2019)
• University of Padova (Jun 2019)

and by others at:

• University of Vermont
• Google Seattle.

The book is described in a paper (of the same title) at the XXI Brazilian Symposium on Formal Methods, 28–30 Nov 2018, which is available here. The paper won the SBMF 2018 Best Paper Award, 1st Place.

Please download Agda and the textbook in advance of the course. Follow all instructions under Getting Started with PLFA:

• install agda, including its emacs mode
• install agda-stdlib
• clone https://github.com/plfa/plfa.github.io.git
• set up plfa as a library

Also follow the instructions under “Fonts in Emacs”. You may want to look at “Building the book” and later instructions, but they are not required.

Philip Wadler is Professor of Theoretical Computer Science at the University of Edinburgh. He is an ACM Fellow and a Fellow of the Royal Society of Edinburgh, 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 60, with more than 20,000 citations to his work according to Google Scholar. He contributed to the designs of Haskell, Java, and XQuery, and is a co-author of Introduction to Functional Programming (Prentice Hall, 1988), XQuery from the Experts (Addison Wesley, 2004) and Generics and Collections in Java (O’Reilly, 2006). He has delivered invited talks in locations ranging from Aizu to Zurich.