[Termtools] New release of CoLoR

[Frédéric Blanqui]

Dear all,

I am pleased to announce a new release of CoLoR, a Coq library of
mathematical definitions and theorems on the well-foundedness of rewrite
relations on first and higher order terms, available on
http://color.inria.fr/, with the following new developments:

- Util/Relation/Tarski: Knaster-Tarski fixpoint theorem

- Term/Lambda/LCompInt: interpretation of positive inductive types as
Tait-Girard computability predicates

- Term/Lambda/LCall: lexicographic ordering on partial function calls

- Term/Lambda/LCompRewrite: definition of higher-order rewriting (with
matching modulo alpha-equivalence) and its associated computability
structure

- Term/Lambda/LCompClos: formalization and correctness proof of the
notion of computability closure for proving the termination of
higher-order rewrite systems (together with beta-reduction), extending
results presented in "Inductive-data-type Systems", by F. Blanqui, J.-P.
Jouannaud and M. Okada, in Theoretical Computer Science 272, p. 41-68, 2002.

Let me remind you that, in Term/Lambda/, lambda-terms, substitution,
alpha-equivalence, etc. are formalized following Curry and Feys
definition (i.e. using named variables and explicit alpha-equivalence)
while, in HORPO/, lambda-terms are formalized using de Bruijn indices.

You can browse the definitions and lemmas (but not the proofs) on
http://color.inria.fr/doc/main.html .

Best regards,

Frédéric.