A termination ordering for higher order rewrite systems
From MaRDI portal
Recommendations
- Higher-Order Orderings for Normal Rewriting
- Normal higher-order termination
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- A recursive path ordering for higher-order terms in η-long β-normal form
- A Monotonic Higher-Order Semantic Path Ordering
Cites work
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A unification algorithm for typed -calculus
- scientific article; zbMATH DE number 3730111 (Why is no real title available?)
- scientific article; zbMATH DE number 48095 (Why is no real title available?)
- scientific article; zbMATH DE number 3993540 (Why is no real title available?)
- Orderings for term-rewriting systems
- Termination of combined (rewrite and λ-calculus) systems
- Termination of term rewriting by interpretation
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Topics in termination
Cited in
(36)- Termination orderings for associative-commutative rewriting systems
- Higher-order rewrite systems and their confluence
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- Abstract data type systems
- scientific article; zbMATH DE number 1615229 (Why is no real title available?)
- Normal higher-order termination
- Simplifying algebraic functional systems
- scientific article; zbMATH DE number 2185672 (Why is no real title available?)
- Harnessing first order termination provers using higher order dependency pairs
- scientific article; zbMATH DE number 3870584 (Why is no real title available?)
- Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations
- Higher-Order Orderings for Normal Rewriting
- Uncurrying for termination and complexity
- The Computability Path Ordering: The End of a Quest
- scientific article; zbMATH DE number 176122 (Why is no real title available?)
- scientific article; zbMATH DE number 1301857 (Why is no real title available?)
- Extension orderings
- The recursive path and polynomial ordering for first-order and higher-order terms
- Bi-rewriting, a term rewriting technique for monotonic order relations
- Topics in termination
- A recursive path ordering for higher-order terms in η-long β-normal form
- Linear second-order unification
- Polymorphic higher-order termination
- Polynomial interpretations for higher-order rewriting
- Graph path orderings
- Higher-Order Termination: From Kruskal to Computability
- Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
- Higher order dependency pairs for algebraic functional systems
- Partial Order Infinitary Term Rewriting
- Uncurrying for Termination
- The practice of logical frameworks
- Could orders be captured by term rewriting systems?
- Rewriting Techniques and Applications
- Currying of order-sorted term rewriting systems
- A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems
- Higher-order proof by consistency
This page was built for publication: A termination ordering for higher order rewrite systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5055816)
