Sous typage structurel en théorie des types à la Martin-Löf

Cette thèse se propose d'étudier les interactions subtiles entre un système de types dépendants et une fonctionnalité concrète que l'ont trouve dans les langages de programmation modernes à savoir le sous-typage structurel. Les principaux résultats métathéoriques sont établis, afin de s'assurer qu'un tel système de types est cohérent et que le typage est décidable. En effet la présence simultanée de différents mécanismes et leurs interactions peut donner lieu à des difficultés. Ces propriétés sont cruciales dans la mesures où ces systèmes de types sont au cœur des systèmes de vérification formelles. Ce travail est destiné à influencer directement le développement d'assistants de preuves comme Coq, et plus largement les outils de vérification basés sur les types dépendants.La thèse comporte trois chapitres introductifs, le premier est une introduction générale, suivi d'un chapitre présentant les théories des types à la Martin-Löf et d'un chapitre présentant le sous-typage dans ce contexte. Le chapitre 4 présente quelques problèmes spécifiques posés par le sous-typage structurel en théorie des types. Le chapitre 5 présente les résultats techniques et développements mécanisés sur lesquels le reste de la thèse s'appuie. Le cœur de la thèse est composé des chapitres 6 et 7 qui comportent les résultats originaux développés dans la thèse :- Une théorie des types étendue avec des équations fonctorielles pour ses constructeurs paramétrés, dont la métathéorie est entièrement formalisée en Coq. Ce développement est une étape intermédiaire importante dans la mesure ou ces équations fonctorielles sont nécessaires pour construire une théorie avec sous-typage non triviale.- Une présentation algorithmique du sous-typage avec type dépendant et la présentation d'une relation de correspondance entre sous-typage explicite et sous-typage implicite, permettant d'établir une sémantique précise pour ce dernier.Enfin le chapitre 8 conclut par des pistes pour de futures recherches.