TY - GEN
T1 - More church-rosser proofs (in Isabelle/HOL)
AU - Nipkow, Tobias
N1 - Publisher Copyright:
© Springer-Verlag Berlin Heidelberg 1996.
PY - 1996
Y1 - 1996
N2 - The proofs of the Church-Rosser theorems for β, η and β ∪ η reduction in untyped λ-calculus are formalized in Isabelle/HOL, an implementation of Higher Order Logic in the generic theorem prover Isabelle. For β-reduction, both the standard proof and the variation by Takahashi are given and compared. All proofs are based on a general theory of commutating relations which supports an almost geometric style of confluence proofs.
AB - The proofs of the Church-Rosser theorems for β, η and β ∪ η reduction in untyped λ-calculus are formalized in Isabelle/HOL, an implementation of Higher Order Logic in the generic theorem prover Isabelle. For β-reduction, both the standard proof and the variation by Takahashi are given and compared. All proofs are based on a general theory of commutating relations which supports an almost geometric style of confluence proofs.
UR - http://www.scopus.com/inward/record.url?scp=84957702937&partnerID=8YFLogxK
U2 - 10.1007/3-540-61511-3_125
DO - 10.1007/3-540-61511-3_125
M3 - Conference contribution
AN - SCOPUS:84957702937
SN - 3540615113
SN - 9783540615118
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 733
EP - 747
BT - Automated Deduction – Cade-13 - 13th International Conference on Automated Deduction, Proceedings
A2 - Slaney, John K.
A2 - McRobbie, Michael A.
PB - Springer Verlag
T2 - 13th International Conference on Automated Deduction, CADE 1996
Y2 - 30 July 1996 through 3 August 1996
ER -