Programming Language Foundations in Agda
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
Part 1: Logical Foundations
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
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.