Programming Language Foundations in Agda

Wen Kokke, Jeremy Siek, Philip Wadler

This book is an introduction to programming language theory using the proof assistant Agda.

Comments on all matters---organisation, material to add, material to remove, parts that require better explanation, good exercises, errors, and typos---are welcome. The book repository is on GitHub. Pull requests are encouraged.

Table of Contents

Front matter

Part 1: Logical Foundations

Part 2: Programming Language Foundations

  • Lambda: Introduction to Lambda Calculus

  • Properties: Progress and Preservation

  • DeBruijn: Intrinsically-typed de Bruijn representation

  • More: Additional constructs of simply-typed lambda calculus

  • Bisimulation: Relating reductions systems

  • Inference: Bidirectional type inference

  • Untyped: Untyped lambda calculus with full normalisation



  • Courses taught from the textbook:

    • Philip Wadler, University of Edinburgh, 2018, 2019

    • David Darais, University of Vermont, 2018

    • John Leo, Google Seattle, 2018--2019

    • Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro (PUC-Rio), 2019

    • Prabhakar Ragde, University of Waterloo, 2019

  • A paper describing the book appeared in SBMF.

This work is licensed under a Creative Commons Attribution 4.0 International License. Some changes were made to the original version in order to adapt its contents to nextjournal.