Pages that link to "Item:Q3801105"

The following pages link to A mechanical proof of the Church-Rosser theorem (Q3801105):

Displaying 16 items.

• A formalization of the Knuth-Bendix(-Huet) critical pair theorem (Q616850) (← links)
• Computer theorem proving in mathematics (Q704001) (← links)
• Viewing \({\lambda}\)-terms through maps (Q740485) (← links)
• Abstract abstract reduction (Q817587) (← links)
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← links)
• A proof of the substitution lemma in de Bruijn's notation (Q1802059) (← links)
• A solution to the PoplMark challenge based on de Bruijn indices (Q1945917) (← links)
• Proof movie -- a proof with the Boyer-Moore prover (Q2366695) (← links)
• The mechanisation of Barendregt-style equational proofs (the residual perspective) (Q2841232) (← links)
• A third-order representation of the \(\lambda\mu\)-calculus (Q2841236) (← links)
• (Q2985126) (← links)
• Proof Pearl: Abella Formalization of λ-Calculus Cube Property (Q4916060) (← links)
• A PVS Theory for Term Rewriting Systems (Q5178962) (← links)
• The Mechanical Verification of a DPLL-Based Satisfiability Solver (Q5179007) (← links)
• The practice of logical frameworks (Q5878905) (← links)
• A theorem prover for a computational logic (Q6488518) (← links)