Le séminaire a lieu à l'Inria Bordeaux.
Les assistants de preuve ont deux types d’applications : la construction de preuves formelles de correction de programmes ou d'algorithmes très complexes (compilateurs et analyseurs statiques, algorithmes distribués, protocoles cryptographiques, etc. ), et celle de preuves formelles de théorèmes requérant l'étude de nombreux cas complexes (théorèmes des quatre couleurs, théorème de Feit-Thompson sur la classification des groupes, conjecture de Kepler sur le rangement optimal des sphère, etc.). Ces preuves sont en général très volumineuses, ce qui pose deux problèmes majeurs. D’abord, aucun être humain ne peut en écrire tous les détails ; ceux-ci sont créés en machine suivant les stratégies et indications fines fournies par l'utilisateur. Ensuite, la confiance en la correction d’une preuve écrite à l'aide d'un assistant de preuve provient de celle qu'on accorde au programme de vérification de preuves présent dans le noyau de cet assistant.
A l'aide de quelques exemples, nous abordons les questions suivantes :
La réponse à ces questions tient en deux aspects : d'un point de vue pratique, développer des « patrons de preuve » similaires aux « patrons de conception » de la programmation ; comprendre la logique mathématique utilisée par l'assistant de preuve et valider la correction de l'algorithme de vérification des preuves.
