A mechanical proof of the Church-Rosser theorem

DOI10.1145/44483.44484zbMath0654.68103OpenAlexW2007471348MaRDI QIDQ3801105

No author found.

Publication date: 1988

Published in: Journal of the ACM (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1145/44483.44484

zbMATH Keywords

combinatory logicBoyer-Moore theorem proverproof checkingChurch-Rosser theorem

Mathematics Subject Classification ID

Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)

Related Items (15)

Proof movie -- a proof with the Boyer-Moore prover ⋮ Unnamed Item ⋮ A formalization of the Knuth-Bendix(-Huet) critical pair theorem ⋮ A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. ⋮ A solution to the PoplMark challenge based on de Bruijn indices ⋮ Proof Pearl: Abella Formalization of λ-Calculus Cube Property ⋮ Computer theorem proving in mathematics ⋮ A PVS Theory for Term Rewriting Systems ⋮ The Mechanical Verification of a DPLL-Based Satisfiability Solver ⋮ A proof of the substitution lemma in de Bruijn's notation ⋮ Viewing \({\lambda}\)-terms through maps ⋮ The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective) ⋮ A Third-Order Representation of the λμ-Calculus ⋮ The practice of logical frameworks ⋮ Abstract abstract reduction

This page was built for publication: A mechanical proof of the Church-Rosser theorem