Paper Info
Title
Machine-checked Proof of the Church-Rosser Theorem for the Lambda Calculus Using the Barendregt Variable Convention in Constructive Type Theory.
Abstract
In this article we continue the work started in [Ernesto Copello, Álvaro Tasistro, Nora Szasz, Ana Bove, and Maribel Fernández. Alpha-structural induction and recursion for the λ-calculus in constructive type theory. Electronic Notes in Theoretical Computer Science, 323:109–124, 2016], deriving in Constructive Type Theory new induction principles for the λ-calculus, using (the historical) first order syntax with only one sort of names for both bound and free variables, and with α-conversion based upon name swapping. The principles provide a flexible framework for mimicking pen-and-paper proofs within the rigorous formal setting of a proof assistant. We here report on one successful application, namely a complete proof of the Church-Rosser Theorem. The whole development has been machine-checked using the system Agda [Ulf Norell. Towards a Practical Programming Language Based on Dependent Type Theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, September 2007].
Year
DOI
Venue
2018
10.1016/j.entcs.2018.10.006
Electronic Notes in Theoretical Computer Science
Keywords
Field
DocType
Lambda Calculus,Formal Metatheory,Type Theory
Discrete mathematics,Lambda calculus,Intuitionistic type theory,Computer science,Free variables and bound variables,Mathematical proof,Agda,Church–Rosser theorem,Calculus,Recursion,Proof assistant
Journal
Volume
ISSN
Citations 
338
1571-0661
0
PageRank 
References 
Authors
0.34
2
3
Name
Order
Citations
PageRank
Ernesto Copello132.05
Nora Szasz2528.48
Álvaro Tasistro3212.99