Montrer l'équivalence de définitions de types et de fonctions automatiquement // Proving the equivalence of type and function definitions automatically

Les preuves formelles sont utilisées en mathématiques mais aussi dans l'industrie pour certifier la correction de protocoles, de programmes et de matériel. L'interopérabilité est une fonctionnalité très importante en informatique et en ingénierie pour éviter la duplication inutile du travail et augmenter la sécurité. Malheureusement, l'interopérabilité entre les systèmes de preuve n'est pas bien développée.
Lors de la traduction des définitions et des preuves d'un système à un autre, l'une des difficultés est d'obtenir quelque chose de facilement utilisable dans le système cible. À cette fin, il est nécessaire d'aligner les définitions du système source avec celles déjà définies dans le système cible.
L'objectif de ce projet est de développer des tactiques de preuve pour prouver formellement dans un assistant à la preuve que deux types sont isomorphes et que deux fonctions sont égales, de sorte qu'on puisse remplacer un type par un autre, et une fonction par une autre.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Formal proofs are used in mathematics but also in the industry for certifying the correctness of protocols, software and hardware. Interoperability is a very important feature in computer science and engineering to avoid useless work duplication and increase safety. Unfortunately, interoperability between proof systems is not well developed.
When translating definitions and proofs from one system to another one, one difficulty is to get something readily usable in the target system. To this end, it is necessary to align the definitions of the source system with those already defined in the target system.
The goal of this project is to develop proof tactics to formally prove in a proof assistant that two types are isomorphic, and that two functions are equal, so that one can replace one by the other.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

Début de la thèse : 01/10/2025
WEB : https://blanqui.gitlabpages.inria.fr/equiv.html

Contrats ED : Programme blanc GS-ISN*Financement de l'INRIA*Programme pour normalien (hors ENS Paris-Saclay) et polytechnicien*Programme pour normalien ENS Paris-Saclay

Université Paris-Saclay GS Informatique et sciences du numérique

580 Sciences et Technologies de l'Information et de la Communication

Formation en logique. Expérience avec un assistant de preuve.
Background in logic. Experience with some proof assistant.