The Coq mailing list

[Frederic Blanqui <Frederic.Blanqui AT loria.fr>]

CoLoR, a Coq Library on Rewriting and termination
-------------------------------------------------

http://www.loria.fr/~blanqui/color.html

I am pleased to announce the release of the first version of CoLoR, a Coq 
Library on Rewriting and termination. Coq is a proof assistant developped at 
INRIA available at http://coq.inria.fr/. The aim of this Coq library is to 
provide the necessary formal basis for certifying the termination witnesses 
searched and built by termination tools like CiME, AProVE, TTT, Cariboo, etc.

For the moment, among other things, it includes:
- a library on vectors
- a library on integer polynomials with multiple variables
- a library on algebraic terms with symbols of fixed arity
- a proof of the termination criterion based on polynomial interpretations
- a proof of the dependancy pairs theorem

The library is likely to evolve and include more developments quickly. 
Contributions on RPO and HORPO are on the way, with a library on finite 
multisets. If you are interested, you can join our working group. Contributions 
to this project are very welcome!

For announcements and discussions, you can subscribe to the CoLoR mailing list 
http://sympa.loria.fr/wwsympa/info/color.

You can download the library and get more information on the CoLoR web page 
http://www.loria.fr/~blanqui/color.html. The library is distributed under the 
terms of the french free software license CeCILL, that is compatible with the 
GNU General Public License.