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.

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