Pages that link to "Item:Q1595924"

The following pages link to More Church-Rosser proofs (in Isabelle/HOL) (Q1595924):

Displaying 21 items.

• A mechanised proof of Gödel's incompleteness theorems using Nominal Isabelle (Q286772) (← links)
• A formalization of the Knuth-Bendix(-Huet) critical pair theorem (Q616850) (← links)
• Abstract abstract reduction (Q817587) (← links)
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← links)
• The Church-Rosser theorem and quantitative analysis of witnesses (Q1627965) (← links)
• A solution to the PoplMark challenge using de Bruijn indices in Isabelle/HOL (Q1945915) (← links)
• A solution to the PoplMark challenge based on de Bruijn indices (Q1945917) (← links)
• A simplified proof of the Church-Rosser theorem (Q2016071) (← links)
• Isabelle's metalogic: formalization and proof checker (Q2055847) (← links)
• A formalization and proof checker for Isabelle's metalogic (Q2108191) (← links)
• Machine-checked proof of the Church-Rosser theorem for the lambda calculus using the Barendregt variable convention in constructive type theory (Q2333314) (← links)
• Operational techniques in PVS -- a preliminary evaluation (Q2703747) (← links)
• Equational Reasoning with Applicative Functors (Q2829262) (← links)
• The mechanisation of Barendregt-style equational proofs (the residual perspective) (Q2841232) (← links)
• More SPASS with Isabelle (Q2914754) (← links)
• (Q2985126) (← links)
• More Church-Rosser proofs (in Isabelle/HOL) (Q4647561) (← links)
• From Search to Computation: Redundancy Criteria and Simplification at Work (Q4916077) (← links)
• A PVS Theory for Term Rewriting Systems (Q5178962) (← links)
• Simplified Reducibility Proofs of Church-Rosser for β- and βη-reduction (Q5178963) (← links)
• A Mechanized Model of the Theory of Objects (Q5428912) (← links)