Pages that link to "Item:Q1127334"
From MaRDI portal
The following pages link to Higher-order rewrite systems and their confluence (Q1127334):
Displayed 37 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)
- Checking overlaps of nominal rewriting rules (Q1744404) (← links)
- Higher-order substitutions (Q1854398) (← links)
- Perpetuality and uniform normalization in orthogonal rewrite systems (Q1854401) (← 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)
- Shallow confluence of conditional term rewriting systems (Q2518609) (← 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)
- Size-based termination of higher-order rewriting (Q4577817) (← links)
- The variable containment problem (Q4645807) (← links)
- Development closed critical pairs (Q4645811) (← 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)
- (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)