Topic description
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/
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.