Action incitative CFC
L'action incitative CFC (pour "Calcul formel certifié")
a été lancée par la direction scientifique de l'INRIA
pour une durée de deux ans: 98 et 99 (voir la présentation
des actions incitatives).
Son but est de mener des recherches pour obtenir des
implantations d'algorithmes de calcul formel qui soient efficaces et
formellement certifiées.
Les équipes participantes:
-
Coq(INRIA Rocquencourt)
-
Cristal(INRIA Rocquencourt)
-
Croap(INRIA Sophia
Antipolis)
-
Foc(équipesCalforetSpidu
LIP6, Paris 6)
Contact: Loïc Pottier
Programme de
l'action.
Réunion des 1er et
2 juillet 98
Les contributions:
-
GbCoq: une implantation certifiée de l'algorithme de
Buchberger
-
FFFC:
factorisation de polynomes dans les corps finis
-
STALMARCK: un
algorithme de calcul booléen
-
Télescopes: des records généralisés définis dans
Coq lui-meme (expérimental).
-
Ctcoqmath: un
développement d'algèbre en Coq et Ctcoq.