Informatique temps réel, robotique et automatique - Fontainebleau

Ingénierie des Systèmes, Matériaux, Mécanique, Énergétique

HERMANT Olivier

DOWEK Gilles

Mathématiques et Systèmes

01/10/2021

Preuve, Assistant de preuve

Proof, Proof assistant

Le but de cette thèse est de travailler sur le problème des mathématiques in- verses pour la bibliothèque de Coq. Plus concrètement :
• des outils ont été développés pour Matita, il s'agit de les adapter aux démonstrations de Coq. En particulier, il est nécessaire de comprendre l'impact, sur ces outils, du polymorphisme d'univers de Coq, qui est le point de divergence majeur avec Matita.
• Il s'agit ensuite d'identifier les theorèmes de Coq dont les preuves ne se traduisent pas en théorie des types simples. Pour chacun de ces théorèmes, une analyse des raisons pourra faire ressortir les principes logiques dont on ne peut se passer et qui vont au-delà de la théorie des types simples.
• Enfin, le travail conduira à aller plus loin (ou plutôt, “moins loin”) que la théorie des types simples. Certaines de ces démonstrations, notamment les Éléments d'Euclide, pourront être traduits dans des sous-fragments de la théorie des types simples, voire en logique des prédicats.
• Une fois tout ceci mis en œuvre, les démonstration de Coq pourront être partagées avec tout système qui s'accordera avec les principes logiques minimaux requis, via Logipedia.
Cette thèse comporte de nombreux aspects novateurs par rapport à l'état de l'art, tant du point de vue théorie (analyse du polymorphisme d'univers, minimisation poussée de la logique, rétro-analyse parcimonieuse des preuves) que pratique (taille des bibliothèques à traiter et à partager). Les contributions associées seront donc de nature académique (publications et partage de preuves), mais aussi logicielle.

See French description

La recherche comme l'industrie manquent d'un cadre logique dans lequel les sous-démonstrations d'un problème complexe pourraient être mises bout à bout et vérifiées comme un tout. La communauté de la démonstration formelle manque d'un standard dans lequel exprimer et échanger les démonstrations. L'objectif de cette thèse est de contribuer à lever ces verrous technologiques.

L'encadrement de cette thèse sera assuré par Olivier Hermant, professeur à MINES ParisTech au Centre de recherche en informatique, et Gilles Dowek, directeur de recherche à Inria Paris-Saclay et au LSV, ENS Paris-Saclay.

Compétences en mathématiques, méthodes formelles, programmation fonctionnelle, Coq ou autre assistant de preuve

See French description

- R. Saillard. “Type Checking in the Lambda-Pi-Calculus Modulo: Theory and Practice”. PhD thesis. MINES ParisTech, 2015.
- F. Thiré. “Interoperability between proof systems using the Dedukti logical framework”. PhD thesis. Université Paris-Saclay, 2020.

Concours pour un contrat doctoral

https://www.adum.fr/script/downloadfile.pl?type=78&ID=34861