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.