index.md

title	layout
Table of Contents	page

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: Inherently 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
• A paper describing the book appeared in SBMF