Combining union, intersection and dependent types in an explicitely typed lambda-calculus

Le sujet de cette thèse est sur le lambda-calcul décoré avec des types, communément appelé « lambda-calcul typé à la Church ». Nous étudions des versions de ce lambda-calcul muni de types intersections, tels que ceux décrits dans le livre « Lambda-calculus with types » de Barendregt, Dekkers et Statman ; les types unions, qui ont été introduits par Plotkin, MacQueen et Sethi ; et les types dépendants, tels qu'ils ont été décrits par Plotkin, Harper et Honsell lorsqu'ils ont introduit le Logical Framework d'Edinbourgh LF. Les types intersections et unions sont un moyen d'exprimer du polymorphisme ad hoc et sont une alternative au polymorphisme paramétrique de Girard. Les types dépendants ont été introduits pour formaliser la logique intuitionniste avec la correspondance de Curry-Howard. Le système de types obtenu peut être enrichi avec une relation de soutypage décidable. La combinaison de ces trois disciplines de type donne lieu à une famille de calculs qui peuvent être paramétrés et classifiés. Nous appelons le système générique le Delta-calcul. Nous discutons ensuite des décisions de conception qui nous ont amené à la formulation de ces calculs, nous étudions leur métathéorie, et nous présentons divers exemples d'applications avant de présenter une implémentation logicielle du Delta-calcul, avec une description des algorithmes de vérification de type, de raffinement, de soutypage, d'évaluation, ainsi que de l'interface en ligne de commande. Ce travail de recherche peut être vu comme un petit pas franchi dans la direction d'une théorie des types alternative pour définir du polymorphisme dans les langages de programmation et dans les assistants de preuve interactifs.