Table of Contents
This book is an introduction to programming language theory, written in Agda. The authors are Wen Kokke and Philip Wadler.
Please send us comments! Comments on all matters—organisation, material we should add, material we should remove, parts that require better explanation, good exercises, errors, and typos—are welcome. Pull requests are encouraged.
Front matter
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