The Computability Path Ordering: The End of a Quest
From MaRDI portal
Publication:3540166
DOI10.1007/978-3-540-87531-4_1zbMath1156.68568OpenAlexW1558388494MaRDI QIDQ3540166
Albert Rubio, Jean-Pierre Jouannaud, Frédéric Blanqui
Publication date: 20 November 2008
Published in: Computer Science Logic (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/inria-00288209v2/file/main.pdf
Logic in computer science (03B70) Mechanization of proofs and logical operations (03B35) Grammars and rewriting systems (68Q42)
Related Items (6)
Harnessing First Order Termination Provers Using Higher Order Dependency Pairs ⋮ Normal Higher-Order Termination ⋮ Jumping and escaping: modular termination and the abstract path ordering ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Simplifying Algebraic Functional Systems ⋮ A Knuth-Bendix-like ordering for orienting combinator equations
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Orderings for term-rewriting systems
- On recursive path ordering
- Adding algebraic rewriting to the untyped lambda calculus
- Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
- Abstract data type systems
- Dependent types for program termination verification
- Termination of term rewriting using dependency pairs
- A Monotonic Higher-Order Semantic Path Ordering
- HORPO with Computability Closure: A Reconstruction
- Automated Termination Analysis for Haskell: From Term Rewriting to Programming Languages
- Higher-Order Orderings for Normal Rewriting
- Polymorphic higher-order recursive path orderings
- Orderings and Constraints: Theory and Practice of Proving Termination
- Computability Closure: Ten Years Later
- Modularity of strong normalization in the algebraic-λ-cube
- Termination of rewriting in the Calculus of Constructions
- Type-based termination of recursive definitions
- Definitions by rewriting in the Calculus of Constructions
- Termination checking with types
- The size-change principle for program termination
- Higher-Order Termination: From Kruskal to Computability
- Logic for Programming, Artificial Intelligence, and Reasoning
- Termination of combined (rewrite and λ-calculus) systems
- Adding algebraic rewriting to the calculus of constructions : Strong normalization preserved
- Rewriting Techniques and Applications
- Rewriting Techniques and Applications
- Inductive-data-type systems
- Calculating sized types
This page was built for publication: The Computability Path Ordering: The End of a Quest
