This book is an introduction to programming language theory, written in Agda. The authors are Wen Kokke and Philip Wadler.

Please send us comments! The text is currrently being drafted. Part I is ready for comment. We plan that Part II will be ready for comment by the end of May.

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 for small fixes are encouraged.

Front matter

Part 1: Logical Foundations

(This part is ready for review. Please send your comments!)

Part 2: Programming Language Foundations

(This part is not yet ready for review.)

Old

In progress

New

Backmatter