Pages that link to "Item:Q4764621"

The following pages link to Residual theory in λ-calculus: a formal development (Q4764621):

Displaying 19 items.

• A formalization of the Knuth-Bendix(-Huet) critical pair theorem (Q616850) (← links)
• Mechanising \(\lambda\)-calculus using a classical first order theory of terms with permutations (Q853738) (← links)
• Developing developments (Q1392147) (← links)
• A formalised first-order confluence proof for the \(\lambda\)-calculus using one-sorted variable names. (Q1401936) (← 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 note on subject reduction in \((\to, \exists)\)-Curry with respect to complete developments (Q2350605) (← links)
• Braids via term rewriting (Q2422032) (← links)
• The mechanisation of Barendregt-style equational proofs (the residual perspective) (Q2841232) (← links)
• Upper bounds for standardizations and an application (Q4254636) (← links)
• A Formalisation of Weak Normalisation (with Respect to Permutations) of Sequent Calculus Proofs (Q4506460) (← links)
• Development closed critical pairs (Q4645811) (← links)
• More Church-Rosser proofs (in Isabelle/HOL) (Q4647561) (← links)
• Proof-relevant π-calculus: a constructive account of concurrency and causality (Q4691184) (← links)
• (Q4808736) (← links)
• Proof Pearl: Abella Formalization of λ-Calculus Cube Property (Q4916060) (← links)
• A PVS Theory for Term Rewriting Systems (Q5178962) (← links)
• The practice of logical frameworks (Q5878905) (← links)
• Variable binding and substitution for (nameless) dummies (Q6151566) (← links)