Abstract FR:

Le typage statique polymorphe est un trait majeur des langages fonctionnels tels que ml. Cependant, les liens entre les types statiques polymorphes inferes par le compilateur et les types dynamiques en cours d'execution est un probleme important pour le developpement de ces langages, par exemple pour des outils de mise au point des programmes. Afin d'apporter un cadre theorique a ce probleme, nous etudions la relation entre inference de type et beta-reduction a travers l'etude complete d'un nouveau systeme de types intersections, appeles types intersections simples. En effet, les systemes de types intersections permettent de typer une large classe de lambda-termes, et semblent donc suffisamment expressifs pour servir de base a l'etude de la reconstruction dynamique de types. Nous commencons par montrer que notre systeme de types possede les proprietes les plus importantes des systemes de types intersections classiques : caracterisation des termes normalisables et normalisables en tete, correction par rapport a un modele de termes, existence d'un type principal pour les lambda-termes normalisables. Nous donnons ensuite une description detaillee de la structure des types principaux, puis un algorithme de reconstruction d'une forme normale a partir d'un type principal. Nous prouvons ainsi l'equivalence entre formes normales et types principaux. La connaissance de la structure des types principaux nous permet alors de simplifier la definition de l'operation d'expansion et de justifier theoriquement cette definition. Nous proposons enfin un semi-algorithme d'inference base sur une reecriture des types. Cette reecriture met en evidence l'equivalence entre l'inference de types et la beta-reduction, puisqu'alors inferer un type pour un lambda-terme revient a mettre un type en forme normale et donc a simuler la normalisation du lambda-terme.