The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Dear all, I am very happy to announce a new release of CoLoR, a Coq
Library on Rewriting and termination, compiling with the new version 8.2
of Coq. The main novelties of this new release (the previous release was
in May 2008) are:

- Correctness, termination and completeness of a syntactic unification
algorithm (file AUnif.v).

- A general dependency graph decomposition theorem (file ADecomp.v).

- Correctness of the dependency graph over-approximation based on
unification (file ADPUnif.v).

- String rewrite system inversion (file SReverse.v).

- Support for using the Coq FSet library (files FSetUtil.v and
AVariables.v).

You can find more details, browse the definitions and lemmas of CoLoR,
or download its sources on the new CoLoR web site http://color.inria.fr/.

The CoLoR library is now about 55000 lines of Coq. It contains about
1070 definitions, 130 tactics and 2800 theorems, and many sub-libraries
of general interest:

    * Termination criteria:
          o polynomial interpretations
          o matrix interpretations (standard, arctic and below-zero)
          o first and higher order recursive path ordering
          o lexicographic and multiset ordering
    * Transformation techniques:
          o dependency graph decomposition based on unification
          o dependancy pairs transformation
          o arguments filtering
          o conversions strings -> algebraic terms -> varyadic terms
          o string rewrite system inversion
    * Term structures:
          o strings
          o algebraic terms with symbols of fixed arity
          o varyadic terms
          o simply typed lambda-terms
    * Data structures:
          o matrices
          o finite multisets
          o integer polynomials with multiple variables
          o vectors/arrays
    * Mathematical structures:
          o semi-rings
          o relations/graphs