Learn Lean 4 with PLFA proofs.
-
Updated
May 2, 2024 - Lean
Learn Lean 4 with PLFA proofs.
A complete proof in Agda of the Church-Rosser theorem for untyped λ-calculus formalizing the methods by Komori-Matsuda-Yamakawa (2014) and the proof by Nagele-van Oostrom-Sternagel (2016); reuses the infrastructure for λ-terms and substitutions provided by the PLFA book
Solutions to the book: Programming Language Foundations in Agda, from Wadler, Philip, Wen Kokke, and Jeremy G. Siek
Answers to the exercises on the book Programming Language Foundations in Agda
Add a description, image, and links to the plfa topic page so that developers can more easily learn about it.
To associate your repository with the plfa topic, visit your repo's landing page and select "manage topics."