The Coq mailing list

[Frederic Blanqui <frederic.blanqui AT inria.fr>]

Dear all,

I am pleased to announce a new release of CoLoR [http://color.inria.fr] 
including in the new sub-directory Term/Lambda:

- LTerm: a formalization of pure lambda-terms with named variables

- LSubs: a formalization of higher-order simultaneous substitution 
following Curry and Feys definition [1]

- LAlpha: a formalization of alpha-equivalence following [1]

- LBeta: a formalization of beta-reduction following [1]

- LComp: an axiomatic formalization of Tait-Girard computability predicates

- LSimple: a formalization of typing with simple types

- LCompSimple: a proof of termination of beta-reduction for simply-typed 
lambda-terms

Frederic.

[1] H. Curry, R. Feys and W. Craig, Combinatory Logic, volume 1, North 
Holland, 1958.