Programming Language Foundations in Agda
Summary
Programming Language Foundations in Agda (PLFA) is a book introducing programming language theory using the Agda proof assistant. The page outlines the book's structure, from logical foundations to denotational semantics, and notes open-source collaboration on GitHub. It also lists related courses and derived works.