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
for some presentation. More papers are provided in
this bibliography. Contributions are
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.
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.)
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)
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)
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
dependancy pairs transformation
dependency graph decomposition
flat context closure
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)