A mechanical proof of the Church-Rosser theorem
From MaRDI portal
Publication:3801105
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
Mechanization of proofs and logical operations (03B35) Combinatory logic and lambda calculus (03B40)
Related Items
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
