Nipkow, Tobias More Church-Rosser proofs (in Isabelle/HOL). (English) Zbl 0958.03011 J. Autom. Reasoning 26, No. 1, 51-66 (2001). Summary: The proofs of the Church-Rosser theorems for \(\beta\), \(\eta\), and \(\beta\cup \eta\) reduction in untyped \(\lambda\)-calculus are formalized in Isabelle/HOL, an implementation of higher order logic in the generic theorem prover Isabelle. For \(\beta\)-reduction, both the standard proof and Takahashi’s are given and compared. All proofs are based on a general theory of commuting relations that supports an almost geometric style of reasoning about confluence diagrams. Cited in 14 Documents MSC: 03B35 Mechanization of proofs and logical operations 03B40 Combinatory logic and lambda calculus 68T15 Theorem proving (deduction, resolution, etc.) (MSC2010) Keywords:lambda-calculus; Church-Rosser proof; theorem proving Software:Isabelle; Isabelle/HOL PDFBibTeX XMLCite \textit{T. Nipkow}, J. Autom. Reasoning 26, No. 1, 51--66 (2001; Zbl 0958.03011) Full Text: DOI