Professor of Theoretical Computer Science
University of Edinburgh
Philip Wadler 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.
Talks at YOW!
(Programming Languages) in Agda = Programming (Languages in Agda) - YOW! Lambda Jam 2019
The most profound connection between logic and computation is a pun. The doctrine of Propositions as Types asserts that propositions correspond to types, proofs to programs, and simplification of proofs to evaluation of programs. The proof of a conjunction is a pair, the proof of a disjunction is a case expression, and the proof of an implication is a lambda expression. Proof by induction is just programming by recursion.
Dependently-typed programming languages, such as Agda, exploit this pun. To prove properties of programming languages in Agda, all we need do is program a description of those languages Agda. Finding an abstruse mathematical proof becomes as simple and as fun as hacking a program. This talk introduces *Programming Language Foundations in Agda*, a new textbook that is also an executable Agda script---and also explains the role Agda is playing in IOHK's new cryptocurrency.
Programming Language Foundations in Agda - YOW! Lambda Jam 2019
Clone the repository at
This is the textbook for the course.
Install Agda, the Agda standard library, and configure the plfa library. This can be done by following the instructions under the heading
Getting Started with PLFA
This course 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.
The textbook is freely available online:
- Programming Language Foundations in Agda
The book has been used for teaching by me at:
- University of Edinburgh (Sep-Dec 2018)
- Pontifícia Universidade Católica do 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
The paper won the SBMF 2018 Best Paper Award, 1st Place.