A Lambda-Free Higher-Order Recursive Path Order
From MaRDI portal
Publication:2988386
DOI10.1007/978-3-662-54458-7_27zbMath1486.68085OpenAlexW2613299215MaRDI QIDQ2988386
Jasmin Christian Blanchette, Daniel Wand, Uwe Waldmann
Publication date: 19 May 2017
Published in: Lecture Notes in Computer Science (Search for Journal in Brave)
Full work available at URL: https://hal.inria.fr/hal-01592189/file/BlanchetteWaldmannWandFoSSaCS.pdf
Related Items
Unnamed Item ⋮ A Lambda-Free Higher-Order Recursive Path Order ⋮ Superposition with lambdas ⋮ Unnamed Item ⋮ A Knuth-Bendix-like ordering for orienting combinator equations
Uses Software
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Uncurrying for termination and complexity
- Paramodulation with non-monotonic orderings and simplification
- Isabelle/HOL. A proof assistant for higher-order logic
- Comparing curried and uncurried rewriting
- Termination of term rewriting using dependency pairs
- SAT solving for termination proofs with recursive path orders and dependency pairs
- A Lambda-Free Higher-Order Recursive Path Order
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates
- Generalized and Formalized Uncurrying
- Certification of Termination Proofs Using CeTA
- The computability path ordering
- Polymorphic higher-order recursive path orderings
- Proving termination with multiset orderings
- A new implementation technique for applicative languages
- Term Rewriting and All That
- The recursive path and polynomial ordering for first-order and higher-order terms
- Computer Aided Verification
- A Higher-Order Iterative Path Ordering
- Nitpick: A Counterexample Generator for Higher-Order Logic Based on a Relational Model Finder
- Completeness in the theory of types
- Rewriting Techniques and Applications
