Contribution: CoLoR

A Coq library on Rewriting and termination

Authors

Description

The aim of this Coq library is to provide the necessary formal basis for certifying termination proofs for rewriting systems

Keywords

termination, rewriting, lambda calculus, polynom, typing, term, multiset, vector, list, rpo, lpo, mpo, horpo, dependency pair, filtering, conversion, manna ness, interpretation, context, substitution, lexicographic, ordering, well founded, algebra, monotony, matrix, string, unification, graph, decomposition

README

This is the CoLoR library on mercredi 11 mars 2009, 12:26:07 (UTC+0800).
Check http://color.inria.fr/ for more recent versions.

CoLoR, a Coq library on rewriting and termination
-------------------------------------------------

The aim of this Coq library (Coq is a proof assistant developped at
INRIA available at http://coq.inria.fr/) is to provide the necessary
formal basis for certifying the termination proof candidates searched
and built by tools like TPA, MatchBox, AProVE, TTT, etc.

Among other things, it includes:

* libraries on mathematical structures in Util/:
	- Relation: binary relations/graphs
		. computation of strongly connected components
		. completion into a total ordering, topological sort
	- Algebra: (ordered) semi-rings

* libraries on data structures in Util/:
	- List: lists
	- Vector: vectors
	- Multiset: finite multisets
	- Polynom: integer polynomials with multiple variables
	- Matrix: matrices over an (ordered) semi-ring

* libraries on term structures in Term/:
	- Varyadic: varyadic terms
	- WithArity: algebraic terms with symbols of fixed arity
	- SimpleType: simply typed lambda-terms with de Bruijn indices
	- String: words

* transformation techniques:
	- DP: dependency pairs transformation and graph decomposition
	- Filter: arguments filterings
	- Conversion: conversions between term structures

* termination criteria:
	- MannaNess: inclusion in some reduction ordering
	- PolyInt: polynomial interpretations
	- MatrixInt: matrix interpretations
	- MPO: multiset path ordering
	- RPO: recursive path ordering
	- HORPO: higher-order recursive path ordering

The library is likely to evolve and include more developments quickly.
For more recent informations, see http://color.inria.fr/.

Contributions to this project are very welcome!

LICENSE: this file describes the license governing this library.
COPYRIGHTS: this file describes the copyrights holders.
INSTALL: this file describes a compilation procedure.
THANKS: thanks to various people for their comments or help.

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

The following scripts provide some statistics:

- get_stat: provides the number of coq lines (including newlines and
comments) for the various kinds of formalizations (mathematical
structures, data structures, etc.)

- coq_stat [<directory>] (default is .): provides the number of
definitions, lemmas, etc.

- coq_contribs <directory>: run coq_stat on every coq contrib

Available files