Soutenance de thèse de Enzo Crance
19 décembre 2023 @ 10 h 00 min - 13 h 00 min
Enzo Crance, Doctorant au sein de l’équipe Gallinette, présentera sa thèse intitulée :
« Meta-Programming for Proof Transfer in Dependent Type Theory »
Le mardi 19 décembre à 10h dans l’amphithéâtre du bâtiment 34, UFR S&T
Jury :
Sandrine Blazy, Professeur des universités, Université de Rennes, IRISA (rapporteur)
Mathieu Boespflug, Chercheur industriel (docteur), Modus Create (invité)
Denis Cousineau, Chercheur industriel (docteur), Mitsubishi Electric R&D Centre Europe, Rennes (co-encadrant)
Assia Mahboubi, Directrice de recherche, Inria, LS2N, Nantes (directrice de thèse)
Guillaume Melquiond, Directeur de recherche, Inria, Université Paris-Saclay, LMF
Anders Mörtberg, Associate professor, Université de Stockholm (rapporteur)
Karl Palmskog, Senior lecturer, KTH Royal Institute of Technology, Stockholm
Nicolas Tabareau, Directeur de recherche, Inria, Nantes Université
Enrico Tassi, Chargé de recherche, Inria Sophia Antipolis Méditerranée, Université Côte d’Azur
Résumé :
En mathématiques comme en informatique, il est d’usage de faire appel à des outils numériques de vérification pour augmenter la confiance dans les preuves et les logiciels. La pratique la plus commune est le test, mais elle est limitée. Les assistants de preuve interactifs sont des outils permettant d’effectuer des preuves avec une grande confiance, laissant l’humain trouver les idées des preuves tout en vérifiant méticuleusement que toutes les étapes de la preuve sont valides. Cette thèse s’inscrit dans une lignée de travaux visant à automatiser les preuves, avec l’objectif final de répandre l’usage des assistants de preuve à la place du test logiciel, partout où cela est possible et pertinent. On s’intéresse ici au partage de théorie formelle entre plusieurs représentations différentes d’un même concept mathématique, ou plusieurs implémentations d’une même spécification. Sur le plan théorique, cette étude s’appuie sur l’analyse de traductions de paramétricité pour le Calcul des Constructions, et en propose une généralisation. Ces résultats s’incarnent dans la conception de deux outils de transfert de preuve, Trakt et Trocq, dont on discute ici l’implémentation, à l’aide du méta-langage Coq-Elpi.
Mots-clés : preuve formelle, automatisation des preuves, méta-programmation
Abstract:
In both mathematics and computer science, it is common practice to use digital verification tools to increase confidence in proofs and software. The most common practice is testing, but it is limited. Interactive proof assistants are tools made to perform proofs with high confidence, letting humans come up with proof ideas while meticulously checking that all proof steps are valid. This thesis is part of a line of work aimed at automating proofs, with the ultimate goal of spreading the use of proof assistants in place of software testing, wherever possible and relevant. Here, we are interested in sharing of formal theory between several different representations of the same mathematical concept, or several implementations of the same specification. From a theoretical point of view, this study is based on the analysis of parametricity translations for the Calculus of Constructions, and proposes a generalisation of them. These results are made concrete in the design of two proof transfer tools, Trakt and Trocq, whose implementation is discussed here, using the Coq-Elpi meta-language.
Keywords: formal proof, proof automation, meta-programming
TH
