iwilare / church-rosser Goto Github PK
View Code? Open in Web Editor NEWA 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
Home Page: https://iwilare.com/bsc-thesis.pdf
License: MIT License