The Coq mailing list

[Olivier Hermant <hermant AT lix.polytechnique.fr>]

---------- Forwarded message ----------
Date: Mon, 14 Mar 2005 09:13:18 +0100 (CET)
From: Frederic Blanqui 
<blanqui AT loria.fr>
To: 
coq-club AT pauillac.inria.fr,
 
rewriting AT ens-lyon.fr,
    
modulogic AT beaune.inria.fr,
 
color AT loria.fr,
 
qsl_tous AT loria.fr,
    
saarlor AT loria.fr,
 
protheo AT loria.fr
Cc: HINDERER Sébastien 
<Sebastien.Hinderer AT loria.fr>
Subject: CoLoR, a Coq Library on Rewriting and termination


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.