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
2 MLstate
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.
Keywords : well-founded relation rewriting termination Coq certification proof
Type de document :
Article dans une revue
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2011, 21 (4), pp.827-859. 〈10.1017/S0960129511000120〉
Liste complète des métadonnées

Littérature citée [83 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/inria-00543157
Contributeur : Frédéric Blanqui <>
Soumis le : mercredi 29 février 2012 - 03:31:29
Dernière modification le : vendredi 25 mai 2018 - 12:02:06
Document(s) archivé(s) le : mercredi 30 mai 2012 - 02:20:06

Fichiers

main.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | LIAMA | CIRAD | INRA

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〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

371

Téléchargements de fichiers

144

Contact


archive-ouverte@inria.fr