Pages that link to "Item:Q1127334"

The following pages link to Higher-order rewrite systems and their confluence (Q1127334):

Displaying 50 items.

• Unifying sets and programs via dependent types (Q408534) (← links)
• Decreasing diagrams and relative termination (Q438562) (← links)
• On proving confluence modulo equivalence for Constraint Handling Rules (Q511019) (← links)
• Infinitary combinatory reduction systems (Q550248) (← links)
• PNL to HOL: from the logic of nominal sets to the logic of higher-order functions (Q714797) (← links)
• Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
• Capture-avoiding substitution as a nominal algebra (Q939160) (← links)
• n-level rewriting systems (Q1084855) (← links)
• Checking overlaps of nominal rewriting rules (Q1744404) (← links)
• Higher-order substitutions (Q1854398) (← links)
• Perpetuality and uniform normalization in orthogonal rewrite systems (Q1854401) (← links)
• Theory and practice of second-order rewriting: foundation, evolution, and SOL (Q2039930) (← links)
• Pure pattern calculus à la de Bruijn (Q2229151) (← links)
• Confluence by critical pair analysis revisited (Q2305423) (← links)
• Soundness and completeness proofs by coinductive methods (Q2362498) (← links)
• Nominal rewriting (Q2373703) (← links)
• Expression reduction systems with patterns (Q2467565) (← links)
• Shallow confluence of conditional term rewriting systems (Q2518609) (← links)
• Pushing the frontiers of combining rewrite systems farther outwards (Q2782485) (← links)
• Nominal Confluence Tool (Q2817917) (← links)
• Normal Higher-Order Termination (Q2946769) (← links)
• ON THE TERMINATION OF RUSSELL’S DESCRIPTION ELIMINATION ALGORITHM (Q3096819) (← links)
• Confluence Competition 2015 (Q3454083) (← links)
• Contextual Natural Deduction (Q3455860) (← links)
• Antimirov and Mosses’s Rewrite System Revisited (Q3602800) (← links)
• (Q4035223) (← links)
• (Q4281465) (← links)
• (Q4447252) (← links)
• Size-based termination of higher-order rewriting (Q4577817) (← links)
• The variable containment problem (Q4645807) (← links)
• Development closed critical pairs (Q4645811) (← links)
• (Q4986740) (← links)
• Rewriting, and equational unification: the higher-order cases (Q5055746) (← links)
• A restricted form of higher-order rewriting applied to an HDL semantics (Q5055839) (← links)
• Higher-order superposition for dependent types (Q5055856) (← links)
• Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding (Q5058367) (← links)
• Algebraic coherent confluence and higher globular Kleene algebras (Q5060195) (← links)
• (Q5089009) (← links)
• Higher-order narrowing with convergent systems (Q5096386) (← links)
• How to prove decidability of equational theories with second-order computation analyser SOL (Q5110922) (← links)
• Cut Elimination, Substitution and Normalisation (Q5213610) (← links)
• Confluence of left-linear higher-order rewrite theories by checking their nested critical pairs (Q5879268) (← links)
• Superposition with lambdas (Q5918381) (← links)
• Superposition with lambdas (Q5919500) (← links)
• A new connective in natural deduction, and its application to quantum computing (Q5925711) (← links)
• Inductive-data-type systems (Q5958292) (← links)
• Type Theory Unchained : Extending Agda with User-Defined Rewrite Rules (Q6079228) (← links)
• Formally verified animation for RoboChart using interaction trees (Q6151624) (← links)
• Superposition for higher-order logic (Q6156638) (← links)
• Sharing proofs with predicative theories through universe-polymorphic elaboration (Q6635505) (← links)