Inria Bordeaux
En libre accès, dans la limite des places disponibles
-

Le séminaire a lieu à l'Inria Bordeaux.

Résumé

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 : 

  • Comment diriger un assistant de preuves de façon à vérifier un programme ou un théorème mathématique ?
  • Comment convaincre une tierce personne qu'un long développement en Coq prouve bien le résultat annoncé ? 

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.

Intervenant(s)

Yves Bertot

Inria Sophia-Antipolis

Pierre Castéran

Labri, Laboratoire Bordelais de Recherche en Informatique