Abstract FR:

Le langage ml est un langage functionnel au polymorphisme parametrique avec synthese de type. De ce fait il presente plus de souplesse que les langages imperatifs usuels fortement types par de meilleures possibilites de modularite. Cependant l'activite de programmation moderne fait fortement ressortir le besoin de nouvelles formes de modularite s'exprimant dans la hierarchisation des donnees, de possibilites plus larges de partage de code permises par le polymorphisme d'inclusion, et de delegation d'operations par la liaison dynamique, caracteristiques propres aux langages objets. Nous proposons dans cette these des elements de description et de formalisation d'un langage fonctionnel polymorphe avec synthese de type comportant des traits orientes objets. Notre approche necessite une reformulation dans un cadre general des formalismes de typage, pour permettre la synthese de type en presence d'une relation entre les types, par l'introduction des schemas de preuve de typage generiques. D'autre part les types des objets seront des types recursifs comprenant une partie enregistrement. Pour les types enregistrement nous portons notre choix sur les records de remy particulierement bien adaptes a la synthese de types. Ces types sont presentes par une theorie equationnelle et la synthese de type requerra entre autre la resolution d'un probleme equationnel avec types recursifs. Nous definirons alors les algebres mu-stables pour donner un sens a l'unification de termes rationnels, associes aux types recursifs, en presence d'une theorie equationnelle. Ce sont des algebres dont les lois sont stables par iteration rationnelle. Nous definissons ensuite les equivalences e-rationnelles pour formaliser un algorithme d'unification pour ces theories. Ce sont des extensions des equivalences rationnelles introduites pour huet pour unifier les termes rationnels. Enfin, nous utilisons a nouveau les algebres mu-stables pour poser les bases d'une etude de la semantique de notre langage