A Lambda-Free Higher-Order Recursive Path Order
From MaRDI portal
A Lambda-Free Higher-Order Recursive Path Order
Recommendations
- Certified Higher-Order Recursive Path Ordering
- Polymorphic higher-order recursive path orderings
- Coq formalization of the higher-order recursive path ordering
- A Higher-Order Iterative Path Ordering
- On recursive path ordering
- The embedding path order for -free higher-order terms
- scientific article; zbMATH DE number 2090310
- A recursive path ordering for higher-order terms in η-long β-normal form
- scientific article; zbMATH DE number 3921961
- Path of subterms ordering and recursive decomposition ordering revisited
Cites work
- A Higher-Order Iterative Path Ordering
- A Lambda-Free Higher-Order Recursive Path Order
- A new implementation technique for applicative languages
- Automated certified proofs with CiME3
- Certification of Termination Proofs Using CeTA
- CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates
- Comparing curried and uncurried rewriting
- Completeness in the theory of types
- Computer Aided Verification
- Generalized and formalized uncurrying
- scientific article; zbMATH DE number 1615229 (Why is no real title available?)
- scientific article; zbMATH DE number 1722716 (Why is no real title available?)
- scientific article; zbMATH DE number 1301857 (Why is no real title available?)
- scientific article; zbMATH DE number 2043542 (Why is no real title available?)
- Isabelle/HOL. A proof assistant for higher-order logic
- Nitpick: a counterexample generator for higher-order logic based on a relational model finder
- Paramodulation with non-monotonic orderings and simplification
- Paramodulation-based theorem proving
- Polymorphic higher-order recursive path orderings
- Proving termination with multiset orderings
- Rewriting Techniques and Applications
- SAT solving for termination proofs with recursive path orders and dependency pairs
- Term Rewriting and All That
- Termination of term rewriting using dependency pairs
- The computability path ordering
- The recursive path and polynomial ordering for first-order and higher-order terms
- Uncurrying for termination and complexity
Cited in
(16)- Superposition for -free higher-order logic
- A Knuth-Bendix-like ordering for orienting combinator equations
- A Lambda-Free Higher-Order Recursive Path Order
- A Monotonic Higher-Order Semantic Path Ordering
- HORPO with Computability Closure: A Reconstruction
- Certified Higher-Order Recursive Path Ordering
- Polymorphic higher-order recursive path orderings
- scientific article; zbMATH DE number 1301857 (Why is no real title available?)
- The recursive path and polynomial ordering for first-order and higher-order terms
- Superposition for lambda-free higher-order logic
- The embedding path order for -free higher-order terms
- scientific article; zbMATH DE number 7204430 (Why is no real title available?)
- Recursive Path Orderings Can Also Be Incremental
- A Higher-Order Iterative Path Ordering
- Superposition with lambdas
- Coq formalization of the higher-order recursive path ordering
Describes a project that uses
Uses Software
This page was built for publication: A Lambda-Free Higher-Order Recursive Path Order
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988386)
