Table of Contents

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. There is a private repository of answers to selected questions on github. Please contact one of the authors if you would like to access it.

Front matter

• Dedication
• Preface
• Getting Started

Part 1: Logical Foundations

• Naturals: Natural numbers
• Induction: Proof by Induction
• Relations: Inductive definition of relations
• Equality: Equality and equational reasoning
• Isomorphism: Isomorphism and Embedding
• Connectives: Conjunction, disjunction, and implication
• Negation: Negation, with intuitionistic and classical logic
• Quantifiers: Universals and existentials
• Decidable: Booleans and decision procedures
• Lists: Lists and higher-order functions

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 reduction systems
• Inference: Bidirectional type inference
• Untyped: Untyped lambda calculus with full normalisation
• Confluence: Confluence of untyped lambda calculus
• BigStep: Big-step semantics of untyped lambda calculus

Part 3: Denotational Semantics

• Denotational: Denotational semantics of untyped lambda calculus
• Compositional: The denotational semantics is compositional
• Soundness: Soundness of reduction with respect to denotational semantics
• Adequacy: Adequacy of denotational semantics with respect to operational semantics
• ContextualEquivalence: Denotational equality implies contextual equivalence

Appendix

• Substitution: Substitution in the untyped lambda calculus

Back matter

• Acknowledgements
• Fonts

Related

Courses taught from the textbook

2025

• Peter Thiemann, Albert-Ludwigs University

2024

• Philip Wadler, University of Edinburgh

2023

• Peter Thiemann, Albert-Ludwigs University
• Philip Wadler, University of Edinburgh

2022

• Andrej Bauer, University of Ljubljana
• Michael Shulman, University of San Diego
• Peter Thiemann, Albert-Ludwigs University
• Philip Wadler, University of Edinburgh

2021

• Favonia, University of Minnesota
• Prabhakar Ragde, University of Waterloo
• Jacques Carette, McMaster University (based on Prabhakar’s)

2020

• William Cook, University of Texas
• Maria Emilia Maietti and Ingo Blechschmidt, Università di Padova
• John Maraist, University of Wisconsin-La Crosse
• Jeremy Siek, Indiana University
• Ugo de’Liguoro, Università di Torino

2019

• Dan Ghica, University of Birmingham
• Adrian King, San Francisco Types, Theorems, and Programming Languages Meetup
• Prabhakar Ragde, University of Waterloo
• Philip Wadler, University of Edinburgh
• Philip Wadler, Pontifícia Universidade Católica do Rio de Janeiro

2018

• David Darais, University of Vermont
• Philip Wadler, University of Edinburgh
• John Leo, Google Seattle

Derived works

• PLFArend: the PLFA book with all code snippets rewritten in Arend.
• PLFaLean: PLFA proofs implemented in Lean 4, covering Parts 2-3 of the v22.08 release of the book.

Please tell us of others!