Contexte : Pourquoi mécaniser la vérification des preuves?

La reproductibilité des résultats est un des piliers de la méthode scientifique. On pourrait imaginer que les sciences exactes échappent à ce problème dans la mesure où la reproductibilité de la preuve d'un théorème ne s'appuie que sur les mécanismes du raisonnement seul, a priori indépendant des conditions d'expérimentations. Cependant, la complexité des preuves en mathématiques et en informatique est telle qu'on ne saurait affirmer sans mentir qu'elles sont parfaitement valides. En effet, la longueur des preuves et l'empilement des concepts nécessaires à leur compréhension rendent extrêmement difficiles leur validation manuelle dans les moindres détails. C'est pourtant ces mêmes détails qui peuvent mettre à mal la validité d'une preuve, et par un jeu de dominos, l'ensemble des résultats qui en sont dérivés. Il n'est ainsi pas rare de trouver des erreurs dans des preuves mathématiques publiées et relues par des pairs. Parce qu'elle omet certains détails, certains paramètres possiblement importants, une preuve sur papier est finalement une sorte d' « expérience de pensée » dont la reproductibilité par un tiers n'est pas nécessairement garantie.

Les assistants de preuve sont des logiciels qui vérifient chaque étape élémentaire de raisonnement utilisée dans une preuve. Ces systèmes connaissent un important essor en mathématiques et en informatique depuis quelques années. Ainsi, le médaillé Fields Vladimir Voevodsky a lancé une ambitieuse entreprise de refonte des mathématiques qui donne un rôle central à l'usage systématique d'un assistant de preuve pour en vérifier chaque théorème et répondre ainsi au problème de fiabilité des preuves mathématiques cité plus tôt en n'acceptant que des preuves « correctes par construction ». C'est l' assistant de preuve Coq, un logiciel developpé depuis 30 ans par des laboratoires français d'informatique, qui a été plébiscité par Voevodsky pour servir de socle à ce projet.

En informatique aussi, les développements logiciels sont connus pour atteindre un degré de complexité dépassant nos capacités de vérification manuelle. Les fameux « bugs » sont issus d'erreurs dans l'écriture des programmes, dont on sait depuis les années 60 que la structure profonde est en correspondance avec celle des preuves mathématiques et qu'il existe aussi pour les programmes des systèmes de preuve garantissant qu'ils sont « corrects par construction ». Là encore, en tant qu'outil pour prouver des programmes, l'assistant de preuve Coq a été distingué par le prestigieux prix Software System Award de l'Association for Computing Machinery américaine.

À la frontière entre informatique et mathématique, l'informatique théorique construit des raisonnements mathématiques complexes sur ses objets d'étude (l'algorithme, la complexité des calculs, la cryptographie, les langages formels, …) et s'intéresse très souvent à la réalisation concrète de ces objets par une machine. À l'aune de la reproductibilité scientifique, le défi de l'informatique théorique est donc double : il lui faut d'une part garantir l'absence d'erreurs dans les preuves de ses théorèmes et d'autre part s'assurer que ses programmes sont des réalisations correctes des objets mathématiques qu'ils sont censés représenter.

À l'heure actuelle, l'usage d'un assistant de preuve dans les développements formels d'informatique théorique est faible. Dans quelques domaines, comme la théorie de la preuve, des langages de programmation ou la vérification des protocoles cryptographiques, son usage se fait de plus en plus courant, dans d'autres domaines, la nature même de cet outil est méconnue. Cette école s'inscrit dans une démarche d'introduction de la preuve mécanisée auprès des communautés de chercheurs en informatique théorique de ces domaines où les assistants de preuve sont encore absents.

École de Printemps d'Informatique Théorique, édition 2015

Cette école de printemps s'adresse à tous les jeunes chercheurs et chercheurs en informatique théorique souhaitant mieux comprendre ce qu'est un assistant de preuve et comment intégrer son usage dans sa recherche. Ainsi, aucune connaissance sur le domaine de la preuve sur ordinateur n'est nécessaire pour suivre cette école .

Les cours seront structurés en huit demi-journées (9h30 - 12h30 et 14h00 - 17h30). Une demi-journée comprendra un cours magistral d'une heure suivie (ou entrelacée) d'une séance de mise en pratique sur machine.

L'ensemble des supports pédagogiques et des logiciels seront disponibles sur une clé USB fournie à votre arrivée.

Les cinq premières demi-journées sont dédiées à la présentation des principaux concepts et techniques utilisés pour mécaniser des preuves sur ordinateur. On s'intéressera particulièrement aux raisonnements par induction, aux preuves d'algorithmes et programmes fonctionnels, impératifs et concurrents.

Les deux demi-journées suivantes porteront sur la mécanisation de deux domaines de l'informatique théorique : la théorie des langages rationnels et la combinatoire.

Enfin, lors de la dernière demi-journée, les participants réfléchiront à la mécanisation de leur propre domaine de recherche dans l'assistant de preuve Coq avec l'aide de l'équipe pédagogique de l'école.

Programme

Lundi 25 mai
Matin Raisonner avec Coq Pierre Letouzey
Après-midi Programmer avec Coq Pierre Letouzey
Mardi 26 mai
Matin Preuve de programmes fonctionnels Matthieu Sozeau
Après-midi Preuve de programmes impératifs Arthur Charguéraud
Mercredi 27 mai
Matin Mécanisation des mathématiques pour l'informatique Assia Mahboubi
Après-midi Relâche
Jeudi 28 mai
Matin Formalisation des automates finis Damien Pous
Après-midi Formalisation de quelques problèmes combinatoires Benjamin Grégoire
Vendredi 29 mai
Matin Votre recherche en Coq

Inscription

Pour s'inscrire, suivez le lien suivant.

Date limite d'inscription: 2015/04/30

Pension complète pour une chambre pour deux: 375 euros.

Pension complète pour un chambre seul: 440 euros.

Localisation

L'école se déroulera à Fréjus dans la villa Clythia.

Pour se détendre entre deux preuves Coq:

  • une piscine chauffée à 25̣ degrés,
  • un parc arboré de 2.5ha,
  • un terrain multisport (volley, tennis, basket).

Partenaires

L'école est financée par:

  • Le GDR Informatique Mathématique
  • Le CNRS
  • L'INRIA
  • La fédération d'informatique fondamentale de Paris Diderot (LIAFA - PPS)

Organisateurs