CoLoR: a Coq Library on Rewriting and termination

CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory, λ-calculus and termination whose correctness has been mechanically checked by the Coq proof assistant. See this paper for some presentation. More papers are provided in this bibliography. Contributions are welcome!

Some developments using CoLoR: Rainbow, HA-Spiral, Spi, ATBR, CPV.

Mailing list: For announcements and discussions about this project, create an account on, log in and subscribe to color.

Download: This library is distributed under the terms of the French free software license CeCILL, that is compatible with the GNU General Public License. Read the conditions of the license before downloading the library. The development version is available on Github.

Last release: version 1.5 for Coq 8.8, 4 May 2018 (see CHANGES)

CoLoR is now available on OPAM. Installation procedure:

Content: BROWSE DEFINITIONS AND STATEMENTS (download CoLoR to see the proofs)

Maintainer: Frédéric Blanqui (INRIA, France)

Contributors: Kim-Quyen Ly (INRIA), Sidi Ould-Biha (INRIA, France), Adam Koprowski (Radboud University, The Netherlands), Johannes Waldmann (Leipzig HTWK, Germany), Sorin Stratulat (Université Paul Verlaine, Metz, France), Julien Bureaux (ENS Paris, France), Pierre-Yves Strub (INRIA, France), Wang Qian (Tsinghua University, China), Zhang Lianyi (Tsinghua University, China), Hans Zantema (Radboud University, Nijmegen, The Netherlands), Jörg Endrullis (Amsterdam Vrije Universiteit, The Netherlands), Stéphane Le Roux (ENS Lyon, France), Léo Ducas (ENS Paris, France), Solange Coupet-Grimal (Université de Provence Aix-Marseille I, France), William Delobel (Université de Provence Aix-Marseille I, France), Sébastien Hinderer (LORIA, France), Frédéric Blanqui (INRIA, France)

Statcounter W3C Validator Last updated on 4 May 2018. Come back to main page.