CoLoR
CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates. Termination is an important property of programs, and is notably required for programs formulated in proof assistants. It is a very active subject of research in the Turing-complete formalism of term rewriting. Over the years, many methods and tools have been developed to address the problem of deciding termination for specific problems (since it is undecidable in general). Ensuring the reliability of those tools is therefore an important issue. We present a library formalising 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 for this software
References in zbMATH (referenced in 19 articles , 1 standard article )
Showing results 1 to 19 of 19.
Sorted by year (- Sternagel, Christian; Thiemann, René: A framework for developing stand-alone certifiers (2015)
- Pottier, François: Syntactic soundness proof of a type-and-capability system with hidden state (2013)
- Braibant, Thomas; Pous, Damien: Deciding Kleene algebras in Coq (2012)
- Blanqui, Frédéric; Koprowski, Adam: CoLoR: a Coq library on well-founded rewrite relations and its application to the automated verifications of termination certificates (2011)
- Gonthier, Georges: Point-free, set-free concrete linear algebra (2011)
- Krauss, Alexander; Sternagel, Christian; Thiemann, René; Fuhs, Carsten; Giesl, Jürgen: Termination of Isabelle functions via termination of rewriting (2011)
- Galdino, André L.; Ayala-Rincón, Mauricio: A formalization of the Knuth-Bendix(-Huet) critical pair theorem (2010)
- Sternagel, Christian; Thiemann, René: Certified subterm criterion and certified usable rules (2010)
- Galdino, André Luiz; Ayala-Rincón, Mauricio: A PVS theory for term rewriting systems (2009)
- Koprowski, Adam: Coq formalization of the higher-order recursive path ordering (2009)
- Koprowski, Adam; Waldmann, Johannes: Max/Plus tree automata for termination of term rewriting (2009)
- L.Galdino, André; Ayala-Rincón, Mauricio: A PVS theory for term rewriting systems (2009)
- Thiemann, René; Sternagel, Christian: Certification of termination proofs using CeTA (2009)
- Waldmann, Johannes: Automatic termination (2009)
- Galdino, André Luiz; Ayala-Rincón, Mauricio: A formalization of Newman’s and Yokouchi’s lemmas in a higher-order language (2008)
- Koprowski, Adam; Zantema, Hans: Certification of proving termination of term rewriting by matrix interpretations (2008)
- Contejean, Evelyne: Modeling permutations in Coq for Coccinelle (2007)
- Barthe, Gilles; Forest, Julien; Pichardie, David; Rusu, Vlad: Defining and reasoning about recursive functions: A practical tool for the Coq proof assistant (2006)
- Coupet-Grimal, Solange; Delobel, William: An effective proof of the well-foundedness of the multiset path ordering (2006)
Further publications can be found at: http://color.inria.fr/biblio.html