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

TL;DR

This paper introduces CoLoR, a Coq library for well-founded rewrite relations, enabling automated verification of termination certificates in proof assistants, thus improving reliability in program termination proofs.

Contribution

It provides a formalized library in Coq for well-founded relations and demonstrates its application to verifying termination certificates automatically.

Findings

Library formalizes key results on well-founded relations

Enables automated verification of termination certificates

Improves reliability of termination proofs in proof assistants

Abstract

Termination is an important property of programs; notably required for programs formulated in proof assistants. It is a very active subject of research in the Turing-complete formalism of term rewriting systems, where many methods and tools have been developed over the years to address this problem. Ensuring reliability of those tools is therefore an important issue. In this paper we present a library formalizing important results of the theory of well-founded (rewrite) relations in the proof assistant Coq. We also present its application to the automated verification of termination certificates, as produced by termination tools.