Marie-Magdeleine, Lionel (2009) Sous-typage coercitif en présence de réductions non-standards dans un système aux types dépendants.
![]() | 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 : |
| ||
---|---|---|---|
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 |