Coq formalization of the higher-order recursive path ordering

DOI10.1007/s00200-009-0105-5zbMath1185.68628OpenAlexW1998337489MaRDI QIDQ843949

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

Related Items (1)

CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates

Uses Software

• Coq
• Automath
• CoLoR
• PoplMark

Cites Work

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

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