Topic description
isabelle_dedukti est un outil qui extrait des preuves d'Isabelle et les traduit en Lambdapi, un langage qui, à son tour, peut être traduit en Coq. Il y a cependant plusieurs problèmes à résoudre pour obtenir quelque chose de cohérent, facilement utilisable et qui passe à l'échelle :
- Isabelle et Coq utilisent tous deux un mécanisme important pour structurer les formalisations : les classes de types et, plus généralement dans Isabelle, les locales. Les classes de types sont une forme restreinte de locales bénéficiant de certaines fonctionnalités supplémentaires. Elles sont largement utilisées pour représenter des structures mathématiques comme des groupes, des anneaux, etc. Cependant, la façon dont les preuves utilisant les locales sont actuellement traduites n'est pas entièrement compatible avec la logique de Coq.
- Pour obtenir des énoncés facilement utilisables en Coq, il est nécessaire d'aligner les définitions d'Isabelle avec celles déjà définies en Coq. Par exemple, un théorème d'Isabelle sur les nombres naturels d'Isabelle doit être traduit en un théorème de Coq sur les nombres naturels de Coq, et non en un théorème de Coq sur la représentation des nombres naturels d'Isabelle en Coq. Pour cela, Lambdapi peut remplacer un symbole Isabelle par une expression Coq. Par exemple, le symbole Isabelle pour le type des nombres naturels par le symbole Coq pour le type des nombres naturels, et le symbole Isabelle pour l'addition sur les nombres naturels par le symbole Coq pour l'addition sur les nombres naturels. Mais, pour qu'un tel remplacement soit valide, il faut prouver que l'expression Coq satisfait les propriétés définissant le symbole Isabelle. Par exemple, que le type représentant les nombres naturels Isabelle dans Coq soit isomorphe au type Coq des nombres naturels, et que l'addition Coq sur les nombres naturels satisfasse la propriété définissant l'addition Isabelle sur les nombres naturels.
- Pour que Coq puisse vérifier la traduction de grandes bibliothèques Isabelle, il sera probablement nécessaire d'utiliser des techniques de partage, de scinder les grosses preuves en parties plus petites, et de paralléliser leur traduction et leur vérification.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
isabelle_dedukti is a tool that extracts proofs from Isabelle and translate them to Lambdapi, a language which, in turn, can be translated to Coq. There are however several problems to solve to get something consistent, readily usable, and that scales up:
- Both Isabelle and Coq use an important mechanism to structure formalizations: type classes and, more generally in Isabelle, locales. Type classes are a restricted form of locales enjoying some additional features. They are heavily used to represent mathematical structures like groups, rings, etc. However, the way proofs using locales are currently translated is not fully compatible with the logic of Coq.
- To get readily usable statements in Coq, it is necessary to align the definitions of Isabelle with those already defined in Coq. For instance, an Isabelle theorem on Isabelle natural numbers should be translated to a Coq theorem on Coq natural numbers, and not to a Coq theorem on the representation of Isabelle natural numbers in Coq. To this end, Lambdapi can replace an Isabelle symbol by a Coq expression. For instance, the Isabelle symbol for the type of natural numbers by the Coq symbol for the type of natural numbers, and the Isabelle symbol for the addition on natural numbers by the Coq symbol for the addition on natural numbers. But, for such a replacement to be valid, one must prove that the Coq expression satisfies the properties defining the Isabelle symbol. For instance, that the type representing Isabelle natural numbers in Coq is isomorphic to the Coq type of natural numbers, and that the Coq addition on natural numbers satisfies the property defining the Isabelle addition on natural numbers.
- In order for Coq to be able to check the translation of large Isabelle libraries, it will probably be necessary to use sharing techniques, split the big proofs in smaller parts, and parallelize their translation and checking.
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
------------------------------------------------------------------------------------------------------------------------------------------------------------------------
Début de la thèse : 01/10/
WEB :
Funding category
Funding further details
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
En cliquant sur "JE DÉPOSE MON CV", vous acceptez nos CGU et déclarez avoir pris connaissance de la politique de protection des données du site jobijoba.com.