MLF est un système de types combinant le polymorphisme implicite de seconde classe de ML avec le polymorphisme de première classe mais explicite du Système F. Nous proposons une représentation des types de MLF qui superpose un graphe acyclique orienté du premier ordre (encodant la structure du type avec partage) et un arbre inversé (encodant la structure de lieurs du type). Cela permet une définition simple et directe de l'instance sur les types, qui se décompose en une instance sur la structure du type, des opérations simples sur l'arbre de lieurs, et un contrôle acceptant ou rejetant ces opérations. En utilisant cette représentation, nous présentons un algorithme d'unification sur les types de MLF ayant une complexité linéaire.<br /><br />Nous étendons ensuite les types graphiques en un système de contraintes graphiques permettant l'inférence de types à la fois pour ML et MLF. Nous proposons quelques transformations préservant la sémantique de ces contraintes, et donnons une stratégie pour utiliser ces transformations afin de résoudre les contraintes de typage. Nous montrons que l'algorithme résultant a une complexité optimale pour l'inférence de types dans MLF, et que, comme pour ML, cette complexité est linéaire sous des hypothèses raisonnables.<br /><br />Enfin, nous présentons une version à la Church de MLF, appelée xMLF, dans laquelle tous les paramètres de fonctions, toutes les abstractions de type et toutes les instantiations de types sont explicites. Nous donnons des règles de réduction pour réduire les instantiations de types. Le système obtenu est confluent lorsque la réduction forte est autorisée, et vérifie la propriété de réduction du sujet. Nous montrons aussi le lemme de progression pour des stratégies faibles de réduction, dont l'appel par nom et l'appel par valeur en restreignant ou non le polymorphisme aux valeurs. Nous proposons un encodage de MLF dans xMLF qui préserve les types, ce qui assure la sureté de MLF.

Dans une première partie, nous définissons un nouveau langage à base fonctionnelle et avec récursion généralisée, en utilisant le système de types avec degrés de Boudol pour éliminer les récursions dangereuses. Ce langage est ensuite étendu par des enregistrements récursifs, puis par des mixins, permettant ainsi de mêler totalement les paradigmes fonctionnels et objets. Nous présentons également une implémentation, MlObj, ainsi que la machine abstraite servant à son exécution.<br /><br />Dans une deuxième partie, nous présentons un nouvel algorithme d'inférence pour les systèmes de types avec intersection, dans le cadre d'une extension du lambda-calcul. Après avoir prouvé sa correction, nous étudions sa généralisation aux références et à la récursion, nous le comparons aux algorithmes d'inférence déjà existants, notamment à celui de Système I, et nous montrons qu'il devient décidable à rang fini.

Nous nous intéressons à une extension de ML avec polymorphisme<br />de première classe, à la manière du Système F.<br />Cette extension, nommée MLF, utilise les annotations de types<br />d'ordre supérieur données explicitement dans le programme pour inférer<br />de manière principale le type le plus général. Toute expression admet<br />ainsi un type principal, qui dépend des annotations présentes<br />initialement dans le programme.<br /><br />Toute expression de ML est typable dans MLF sans annotation<br />supplémentaire. Les expressions du Système F sont encodées de<br />manière systématique dans MLF en supprimant les abstractions<br />et les applications de types, et en traduisant les annotations<br />de types dans le langage de types de MLF.<br />De plus, les paramètres de lambda-abstractions qui ne sont pas<br />utilisés de manière polymorphe n'ont pas besoin d'être annotés.