The following pages link to Inductive-data-type systems (Q5958292):
Displaying 16 items.
- Introducing \(\llparenthesis\lambda\rrparenthesis\), a \(\lambda \)-calculus for effectful computation (Q831147) (← links)
- An initial algebra approach to term rewriting systems with variable binders (Q853743) (← links)
- Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility (Q896904) (← links)
- Expression reduction systems with patterns (Q2467565) (← links)
- Semantic foundations for generalized rewrite theories (Q2503334) (← links)
- Normal Higher-Order Termination (Q2946769) (← links)
- The algebra of recursive graph transformation language UnCAL: complete axiomatisation and iteration categorical semantics (Q3130301) (← links)
- Strong normalisation in two Pure Pattern Type Systems (Q3520143) (← links)
- The Computability Path Ordering: The End of a Quest (Q3540166) (← links)
- Size-based termination of higher-order rewriting (Q4577817) (← links)
- Termination checking with types (Q4659886) (← links)
- Remarks on Isomorphisms of Simple Inductive Types (Q4924549) (← links)
- (Q5018496) (← links)
- Complete algebraic semantics for second-order rewriting systems based on abstract syntax with variable binding (Q5058367) (← links)
- (Q5094148) (← links)
- The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type (Q5111301) (← links)
