LogoLogo

Marie-Magdeleine, Lionel. Sous-typage coercitif en présence de réductions non-standards dans un système aux types dépendants

Marie-Magdeleine, Lionel (2009) Sous-typage coercitif en présence de réductions non-standards dans un système aux types dépendants.

[img]PDF - nécessite un logiciel de visualisation PDF comme GSview, Xpdf or Adobe Acrobat Reader
1035Kb

Résumé en francais

La théorie des types est une discipline au croisement de la logique, des mathématiques et de l'informatique. Elle peut servir de support au développement de programme "zéro faute". L'objet de cette thèse est d'étudier l'extension d'un système aux types dépendants UTT (comprenant notamment des types inductifs) par une relation de récriture concernant un fragment du calcul, à savoir les types finis. Nous nous assurons d'abord que les propriétés de normalisation forte, de confluence et de préservation du type sont toujours préservées malgré l'ajout de la réduction. Ensuite nous enrichissons ce système par la notion de sous-typage coercitif vue comme un mécanisme d'abréviation et effectuons la preuve de conservativité pour le système enrichi du sous-typage par rapport au système de base. L'intérêt d'un tel système est qu'il améliora l'efficacité des assistants à la preuve et offrira un bon cadre pour l'étude des problèmes faisant intervenir des ensembles finis (combinatoire, manipulation de graphe etc).

Sous la direction du :
Directeur de thèse
Soloviev, Sergei
Ecole doctorale:Mathématiques, informatique, télécommunications de Toulouse (MITT)
laboratoire/Unité de recherche :Institut de Recherche en Informatique de Toulouse (IRIT), UMR 5505
Mots-clés libres :Théorie des types - Sous-typage coercitif - Types dépendants - Récriture
Sujets :Informatique
Déposé le :27 Oct 2010 17:26