Coq formalization of the higher-order recursive path ordering

DOI10.1007/S00200-009-0105-5MaRDI QIDQ843949zbMATH OpenOpenAlexFDO

Authors Adam Koprowski

Publication date 18 January 2010

Published in Applicable Algebra in Engineering, Communication and Computing (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/s00200-009-0105-5

zbMATH Keywords

CoqHigher-order rewritingHORPO

Mathematics Subject Classification ID

Recommendations

• Certified Higher-Order Recursive Path Ordering
• scientific article; zbMATH DE number 2185669
• The computability path ordering
• A Lambda-Free Higher-Order Recursive Path Order
• Polymorphic higher-order recursive path orderings

Cites work

• scientific article; zbMATH DE number 1722711 (Why is no real title available?)
• scientific article; zbMATH DE number 2185669 (Why is no real title available?)
• scientific article; zbMATH DE number 42059 (Why is no real title available?)
• scientific article; zbMATH DE number 512769 (Why is no real title available?)
• scientific article; zbMATH DE number 1042221 (Why is no real title available?)
• scientific article; zbMATH DE number 3400430 (Why is no real title available?)
• A formulation of the simple theory of types
• An effective proof of the well-foundedness of the multiset path ordering
• Certification of Automated Termination Proofs
• Certification of Proving Termination of Term Rewriting by Matrix Interpretations
• Certified Higher-Order Recursive Path Ordering
• HORPO with Computability Closure: A Reconstruction
• Higher-Order Orderings for Normal Rewriting
• Intensional interpretations of functionals of finite type I
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Orderings for term-rewriting systems
• Polymorphic higher-order recursive path orderings
• Program extraction from normalization proofs
• Program extraction from proofs of weak head normalization
• Proving open properties by induction
• Term Rewriting and All That
• Theorem Proving in Higher Order Logics
• Types for Proofs and Programs
• What's so special about Kruskal's theorem and the ordinal \(\Gamma{}_ 0\)? A survey of some results in proof theory

Cited in

(6)

• scientific article; zbMATH DE number 2185669 (Why is no real title available?)
• An effective proof of the well-foundedness of the multiset path ordering
• Rewrite orderings for higher-order terms in \(\eta\)-long \(\beta\)-normal form and the recursive path ordering
• Certified Higher-Order Recursive Path Ordering
• A Lambda-Free Higher-Order Recursive Path Order
• CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates

Describes a project that uses

Uses Software

• PoplMark
• CoLoR
• Automath
• Coq

This page was built for publication: Coq formalization of the higher-order recursive path ordering

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q843949)