Bienvenue aux Mines Paristech
Bienvenue à MINES ParisTech
Newsletter International
Website
Théorie & Pratique
Vous êtes

webTV

Lecture

Certificat exécutif : digital native, 3 questions à...

Lecture

Certificat exécutif : digital native, 3 questions à...

Lecture

Mastère Spécialisé AIMove: Artificial Intelligence and Movement in Industries and Creation

Lecture

Olivier Remy, third year student of the Corps des Mines

Lecture

Le Forum mécatronique 2019

+ Toutes les vidéos

Partager

MATHÉMATIQUES INVERSÉES DES DÉMONSTRATIONS COQ

MATHÉMATIQUES INVERSÉES DES DÉMONSTRATIONS COQ

Inverse mathematics for the CoQ proofs

Proposition de thèse

Spécialité

Informatique temps réel, robotique et automatique - Fontainebleau

Ecole doctorale

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

Directeur de thèse

HERMANT Olivier

Co-encadrant

DOWEK Gilles

Unité de recherche

Mathématiques et Systèmes

ContactOlivier Hermant
Date de validité

01/10/2021

Site Web
Mots-clés

Preuve, Assistant de preuve

Proof, Proof assistant

Résumé

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

Contexte

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.

Encadrement

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.

Profil candidat

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

See French description

Références

- 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.

Type financement

Concours pour un contrat doctoral

Document PDF

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

Retour à la liste des propositions

actualité

EcorcAir et les platanes du Quartier latin

Formation EcorcAir et les platanes du Quartier latin Vendredi 2 avril 2021, dernier jour de cours, en présentiel,…
> En savoir +

Félicitations à Rabab Akkouche

Formation Félicitations à Rabab Akkouche 16 candidats étaient en lice, dont 10 doctorants et docteurs…
> En savoir +

Prix de thèses de prospective de la Fondation 2100

Formation Prix de thèses de prospective de la Fondation… La cérémonie s'est déroulée le 9 février, sous la présidence…
> En savoir +

Femmes de science

Formation Femmes de science   Chercheuses confirmées, doctorantes ou élèves ingénieures, elles font la…
> En savoir +

Quelle empreinte environnementale pour notre avenir énergétique ?

Formation Quelle empreinte environnementale pour notre… Le doctorat est un exercice académique codifié qui aboutit à…
> En savoir +

+ Toutes les actualités

contact

Alexandra BELUS
Direction de l'Enseignement
Service du Doctorat
> envoyer un mail

Plan du site
MINES
ParisTech

60, Boulevard Saint-Michel
75272 PARIS Cedex 06
Tél. : +33 1 40 51 90 00

Implantations
Mentions légales | efil.fr | ©2012 MINES ParisTech | +33 1 40 51 90 00 |