Types union, intersection, et dépendants dans le lambda-calcul explicitement typé

The subject of this thesis is about lambda-calculus decorated with types, usually called "Church-style typed lambda-calculus". We study this lambda-calculus enhanced with Intersection types, as described by Barendregt, Dekkers and Statman in the book "Lambda-calculus with Types"; Union types, as introduced by Plotkin, MacQueen and Sethi; and Dependent types, as described by Plotkin, Harper and Honsell when they introduced the Edinburgh Logical Framework LF. Intersection and union types are a way to express ad hoc polymorphism and are an alternative to the parametric polymorphism of Girard. Dependent types were introduced as a way to formalize intuitionistic logic using the "proof-as-lambda-terms / formulas-as-types" Curry-Howard principle. The resulting type system can be enriched with a decidable subtyping relation. Combining these three type disciplines gives rise to a family of calculi that can be parametrized and classified: we call the resulting system the Delta-calculus. We then discuss the design decisions which have led us to the formulation of these calculi, study their metatheory, and provide various examples of applications; and we finally present a software implementation of the Delta-calculus, with a description of the type checker, the refinement algorithm, the subtyping algorithm, the evaluation algorithm and the command-line interface. This work can be understood as a little step toward an alternative type theory to defining polymorphic programming languages and interactive proof assistants.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