A termination ordering for higher order rewrite systems
From MaRDI portal
Publication:5055816
DOI10.1007/3-540-59200-8_45zbMATH Open1503.68134OpenAlexW2012355197MaRDI QIDQ5055816FDOQ5055816
Authors: Olav Lysne, Javier Piris 
Publication date: 9 December 2022
Published in: Rewriting Techniques and Applications (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/3-540-59200-8_45
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
- Title not available (Why is that?)
- The lambda calculus. Its syntax and semantics. Rev. ed.
- Orderings for term-rewriting systems
- Title not available (Why is that?)
- A unification algorithm for typed \(\overline\lambda\)-calculus
- Topics in termination
- Title not available (Why is that?)
- A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification
- Termination of combined (rewrite and λ-calculus) systems
- Termination of term rewriting by interpretation
Cited In (34)
- Higher order dependency pairs for algebraic functional systems
- Linear second-order unification
- Higher-Order Termination: From Kruskal to Computability
- Partial Order Infinitary Term Rewriting
- Higher-order proof by consistency
- Title not available (Why is that?)
- Harnessing first order termination provers using higher order dependency pairs
- Currying of order-sorted term rewriting systems
- The Computability Path Ordering: The End of a Quest
- Normal higher-order termination
- Uncurrying for termination and complexity
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- Higher-order rewrite systems and their confluence
- Could orders be captured by term rewriting systems?
- Abstract data type 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
- Title not available (Why is that?)
- Graph path orderings
- Simplifying algebraic functional systems
- A Simplified Application of Howard’s Vector Notation System to Termination Proofs for Typed Lambda-Calculus Systems
- Title not available (Why is that?)
- The recursive path and polynomial ordering for first-order and higher-order terms
- Uncurrying for Termination
- Extension orderings
- Higher-Order Orderings for Normal Rewriting
- Title not available (Why is that?)
- Topics in termination
- Bi-rewriting, a term rewriting technique for monotonic order relations
- The practice of logical frameworks
- A recursive path ordering for higher-order terms in η-long β-normal form
Uses Software
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)
