A termination ordering for higher order rewrite systems
From MaRDI portal
Publication:5055816
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
- 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?)
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- A unification algorithm for typed -calculus
- 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
(34)- The practice of logical frameworks
- A recursive path ordering for higher-order terms in η-long β-normal form
- Higher order dependency pairs for algebraic functional systems
- Linear second-order unification
- Higher-Order Termination: From Kruskal to Computability
- Partial Order Infinitary Term Rewriting
- scientific article; zbMATH DE number 2185672 (Why is no real title available?)
- Higher-order proof by consistency
- Harnessing first order termination provers using higher order dependency pairs
- The Computability Path Ordering: The End of a Quest
- Uncurrying for termination and complexity
- Normal higher-order termination
- Currying of order-sorted term rewriting systems
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- Higher-order rewrite systems and their confluence
- Abstract data type systems
- Could orders be captured by term rewriting systems?
- Rewriting Techniques and Applications
- Combining Typing and Size Constraints for Checking the Termination of Higher-Order Conditional Rewrite Systems
- Termination Proof of S-Expression Rewriting Systems with Recursive Path Relations
- Termination orderings for associative-commutative rewriting systems
- Polynomial interpretations for higher-order rewriting
- scientific article; zbMATH DE number 3870584 (Why is no real title available?)
- Simplifying algebraic functional systems
- Graph path orderings
- A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems
- scientific article; zbMATH DE number 176122 (Why is no real title available?)
- The recursive path and polynomial ordering for first-order and higher-order terms
- Extension orderings
- Uncurrying for Termination
- Higher-Order Orderings for Normal Rewriting
- scientific article; zbMATH DE number 1615229 (Why is no real title available?)
- Topics in termination
- Bi-rewriting, a term rewriting technique for monotonic order relations
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)
