The Coq mailing list

[Frederic Blanqui <blanqui AT loria.fr>]

I'm happy to announce a new release of CoLoR compiling with Coq 8.1.

It can be downloaded on http://color.loria.fr/.

This new release in particular includes:

- developments by Stephane Le Roux:
        . more functions and lemmas on lists
        . paths, sub-relations, etc.
        . decidability of transitive closure
        . linear extension of a strict ordering

- developments by Frederic Blanqui:
        . modularity results on termination
        . termination criterion based on dependency graph cycles

The changes wrt the previous releases are detailed in 
http://color.loria.fr/CHANGES.CoLoR.

Definitions and theorems can be browsed on 
http://color.loria.fr/doc/main.html.

The development version is available on 
http://gforge.inria.fr/projects/color/.

Content of the CoLoR library:

    * Termination criteria:
          o dependency graph cycles [Blanqui]
          o higher-order recursive path ordering [Koprowski]
          o recursive path ordering [Coupet-Grimal,Delobel]
          o multiset ordering [Koprowski]
          o polynomial interpretations [Hinderer]

    * Transformation techniques:
          o dependancy pairs [Blanqui]
          o rule elimination [Blanqui]
          o arguments filtering [Blanqui]
          o conversion from algebraic to varyadic terms [Blanqui]

    * General libraries:
          o simply typed lambda-terms [Koprowski]
          o finite multisets [Koprowski]
          o varyadic terms [Blanqui]
          o algebraic terms with symbols of fixed arity [Hinderer,Blanqui]
          o integer polynomials with multiple variables [Hinderer]
          o vectors [Hinderer,Blanqui]
          o lists, relations, etc.