| Pierre Castéran |  |
 |
Date de l'exposé : 3 décembre 2004
Preuves interactives de théorèmes et développement de programmes certifiés
L'exposé se veut une introduction à l'assistant de démonstration Coq, ( http://coq.inria.fr ) ainsi qu'au formalisme sur lequel se base cet outil : le Calcul des Constructions Inductives. Des exemples, empruntés aux mathématiques ou a l'algorithmique, montreront la puissance d'expression de ce formalisme.
