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

• Dedication

• Preface

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 reductions systems

• Inference: Bidirectional type inference

• Untyped: Untyped lambda calculus with full normalisation

Backmatter

• Acknowledgements

• Fonts: Test page for fonts

• Statistics: Line counts for each chapter

Related

• 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.