Traduire les preuves Coq ou Lean dans Isabelle/HOL // Translating Coq or Lean proofs to Isabelle/HOL

Il existe déjà des traducteurs de systèmes basés sur la théorie des types simples vers des systèmes basés sur la théorie des types dépendants. Cependant, il n'existe actuellement aucun traducteur dans l'autre sens : des systèmes basés sur la théorie des types dépendants vers des systèmes basés sur la théorie des types simples. Le problème est que les systèmes basés sur la théorie des types simples ne présentent pas de types dépendants de première classe. Un type dépendant est un type qui peut dépendre de certaines valeurs. Par exemple, le type des vecteurs d'une certaine dimension.

Pour traduire les définitions et les preuves d'un système basé sur la théorie des types dépendants vers un système basé uniquement sur la théorie des types simples, il faut donc trouver un moyen d'éliminer l'utilisation des types dépendants. Ce n'est peut-être pas toujours possible, mais nous pouvons rechercher une classe suffisamment large de définitions et de preuves à partir de laquelle les types dépendants peuvent être éliminés. Par exemple, le type des vecteurs de dimension n pourrait être remplacé par le sous-type des listes de longueur n.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

There already exist translators from systems based on simple type theory to systems based on dependent type theory. However, there is currently no translator in the other way around: from systems based on dependent type theory to systems based on simple type theory. The problem is that systems based on simple type theory do not feature first-class dependent types. A dependent type is a type that can depend on some values. For instance, the type of vectors of some given dimension.

To translate the definitions and proofs of a system based on dependent type theory to a system based solely on simple type theory, one therefore has to find a way to eliminate the uses of dependent types. This might not be always possible, but we can look for a large enough class of definitions and proofs from which dependent types can be eliminated. For instance, the type of vectors of dimension n could be replaced by the subtype of lists of length n.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------

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

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

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.