CoLoR is a library of formal mathematical definitions and proofs of theorems on rewriting theory 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, Spi, ATBR, CPV.

**Mailing list:** For announcements and discussions
about this project, create an account
on https://sympa.inria.fr/, 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 here.

**Last release:** version 1.2, 26 January 2016 (see CHANGES)

CoLoR is now available on OPAM. Installation procedure:

opam repo add coq-released https://coq.inria.fr/opam/released

opam update

opam install --jobs=$n coq-color # it takes 8'18" on my computer with $n=20

**Content:**
BROWSE DEFINITIONS AND THEOREMS

__Logic:__- libraries providing basic meta-theorems and tactics (e.g. irreflexivity) on propositions and equality, both for intuitionistic and classical logic, the statement of the axiom of dependent choice, etc.

__Mathematical structures:__- finite and infinite sets: cardinal of a finite set, infinite pigeon-hole principle, infinite Ramsey theorem
- infinite relations/graphs: an extensive library of definitions and theorems on relations including basic operations like union/intersection/composition/iteration or reflexive/transitive/symmetric closure, their relations, the notions of finite path, cycle, strongly connected component, infinite path/rewrite sequence, etc.
- finite relations/graphs: adjacency matrix, computation and topological sorting of strongly connected components, etc.
- (quasi) orderings: linear extension of a finite acyclic relation, Tarski's fixpoint theorem (in a complete lattice, any monotone function has a least/greatest fixpoint), etc.
- well-founded relations: preservation of termination for commuting relations, maximal reduction length of an element wrt a well-founded finitely branching relation, relation between the classical notion of termination (absence of infinite paths) and the intuitionistic one (inductive accessibility), etc.
- (ordered) semi-rings: a library on semi-rings and ordered semi-rings, and its instantiation on various number data structures (natural numbers, integers, arctic/tropical numbers, etc.)

__Data structures:__- libraries extending the Coq standard library on various data structures: booleans, natural numbers, integers, pairs, lists, vectors, finite sets, finite maps, sets, relations, etc.
- natural numbers: list of natural numbers smaller than some bound, least natural number satisfying some property, logarithmic to base 2, decidability of equality on bigN, maximum/minimum of a list of natural numbers, etc.
- lists: an extensive library extending the Coq standard library on lists including many functions and theorems on lists including for instance the number of occurrences of an element, lists with no duplicated elements, a constructive proof of the pigeon-hole principle, lemmas on the permutation of elements, etc.
- vectors: an extensive library on vectors including many basic functions and theorems on vector manipulation, vector product/lexicographic ordering, vector arithmetic, vector components filtering and permutation
- matrices: a library on matrices including basic functions and theorems on matrix arithmetic
- finite multisets: a library on finite multisets including a proof that the multiset extension of a well-founded relation is well-founded
- polynomials with multiple variables: a library on integer polynomials with multiple variables including basic functions and theorems on polynomial arithmetic, positivity and monotony
- finite graphs: a library on finite graphs including a certified algorithm for computing its transitive closure (using a successor function representation) or its strongly connected components (using the adjacency matrix representation)

__Term structures:__- strings/words: definition of basic notions like context and rewriting
- varyadic terms (first-order terms with function symbols taking an arbitrary number of arguments): definition of basic notions like substitution, context, rewriting on varyadic terms
- algebraic terms with function symbols of fixed arity: this is the most developed library on terms including many definitions and theorems on terms and term rewrite relations like the basic notions of substitution, context, subterm, position, cap and aliens, dependency pair, etc.; the notion of model/interpretation (universal algebra); a certified algorithm for matching; a certified algorithm for unification; etc.
- simply typed λ-terms with de Bruijn indices
- pure and simply typed λ-terms with named variables and explicit α-equivalence: definitions and properties of the basic notions of (higher-order) substitution, α-equivalence, β-reduction, etc.; the equivalence of various definitions of α-equivalence (Curry-Feys, Church, Krivine, Gabbay-Pitts); Girard computability predicates; computability closure; strong normalization of β-reduction and higher-order rewrite systems (e.g. Gödel' system T)

__Transformation techniques:__- conversion string → algebraic term → varyadic term (CoLoR provides in particular a translation from CoLoR algebraic terms to Coccinelle terms to allow the reusability of Coccinelle results in CoLoR)
- reversal of SRSs and unary TRSs
- arguments filtering
- dependancy pairs transformation
- dependency graph decomposition
- semantic labeling
- flat context closure

__(Non-)Termination criteria:__- first and higher order recursive path ordering (RPO and HORPO)
- integer polynomial interpretations
- integer/arctic/tropical matrix interpretations
- computability closure for higher-order rewrite systems
- loops (a decision procedure for verifying that a given rewrite sequence is a loop)

**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)

Last updated on 26 January 2016. Come back to main page.