Skip to Main content Skip to Navigation
Journal articles

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

Frédéric Blanqui 1 Adam Koprowski 2
1 FORMES - Formal Methods for Embedded Systems
LIAMA - Laboratoire Franco-Chinois d'Informatique, d'Automatique et de Mathématiques Appliquées, Inria Paris-Rocquencourt
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.
Document type :
Journal articles
Complete list of metadatas

Cited literature [83 references]  Display  Hide  Download

https://hal.inria.fr/inria-00543157
Contributor : Frédéric Blanqui <>
Submitted on : Wednesday, February 29, 2012 - 3:31:29 AM
Last modification on : Tuesday, March 17, 2020 - 3:25:33 AM
Long-term archiving on: : Wednesday, May 30, 2012 - 2:20:06 AM

Files

main.pdf
Files produced by the author(s)

Identifiers

Collections

Citation

Frédéric Blanqui, Adam Koprowski. CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verification of termination certificates. Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2011, 21 (4), pp.827-859. ⟨10.1017/S0960129511000120⟩. ⟨inria-00543157⟩

Share

Metrics

Record views

547

Files downloads

410