# 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

### 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: 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

Fonts: Test page for fonts

Statistics: Line counts for each chapter

### Related

Courses taught from the textbook:

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.