FoCaLiZe
Specifying, Programming
and Proving
Computer Algebra libraries

Here you can find some of my works in FOCAL:

Phd Thesis (in French).
Coq archive of mixDrecs.
The sources described in the Phd Thesis are written in Coq 6.3.1.
They are given here in Coq 8.0 (major concrete syntax changes wrt the original version).
Translation has been performed by the automatic translator of Coq 8.0.

See the home page of the project for more information.

Last modification: Jan 07 2005