Typage statique, Langage dynamique, Inférence de type, Types ensemblistes, Sous-typage sémantique, Typage d'occurrence, Rétrecissement de type, Polymorphisme, Types intersection, Types union

Cette thèse porte sur la conception d'un système de type basé sur les types ensemblistes et visant à typer les langages dynamiques, tels que JavaScript, Python ou Elixir. L'utilisation des types ensemblistes est motivée par leur expressivité : ils sont dotés d'une relation de sous-typage qui prend en charge intersections, unions et négations. Cela permet de capturer de nombreux comportements idiomatiques des langages dynamiques : les types intersection sont utilisés pour capturer les comportements surchargés, et les types union et négation ouvrent la voie vers un typage précis des type-cases (tests de type dynamiques) via l'utilisation de techniques de rétrécissement de types. Les types ensemblistes peuvent également être étendus avec des variables de type afin d'implémenter du polymorphisme paramétrique, permettant la conception d'un système de types modulaire dans lequel les définitions sont typées séquentiellement. Cependant, les types ensemblistes sont généralement utilisés dans un langage où les fonctions doivent être explicitement annotées par leur type. Nous nous débarrassons de cette contrainte en travaillant sur un lambda-calcul sans annotation de type. À la place, un algorithme d'inférence est chargé de reconstruire le type des fonctions. Dans la première partie de ce manuscrit, nous passons en revue les fondements des types ensemblistes et présentons notre langage, un lambda-calcul par appel par valeur avec paires et type-cases, et discutons des défis posés par le typage d'un tel langage. La deuxième partie contient la formalisation de base (et les preuves) du système de types. Le premier système de type que nous définissons est purement déclaratif. Il combine plusieurs règles inspirées de la déduction naturelle, en particulier : l'élimination de l'union, l'introduction de l'intersection, l'instanciation et la généralisation. Nous prouvons la sûreté du typage de ce système : un programme typeable se réduit toujours à une valeur de même type ou diverge. Nous définissons ensuite un système de types algorithmique (déterministe) équivalent au système déclaratif, mais qui prend comme entrée supplémentaire un arbre d'annotations qui spécifie, entre autres, les types des paramètres des lambda-abstractions. Enfin, nous définissons un algorithme de reconstruction qui vise à reconstruire les arbres d'annotations. Dans la dernière partie de ce manuscrit, nous nous concentrons sur certains aspects pratiques. Nous discutons de certaines extensions et optimisations du système de types algorithmique et de l'algorithme de reconstruction, et nous présentons un prototype d'implémentation. Nous évaluons ce prototype sur plusieurs exemples, en soulignant ses forces et ses faiblesses, et en le comparant à d'autres approches.