Typage polymorphe d'un langage algorithmique

The polymorphic type discipline, as in the ML language, fits well within purely applicative languages, but does not extend naturally to the main feature of algorithmic languages: in-place update of data structures. Similar typing difficulties arise with other extensions of applicative languages: logical variables, communication channels, continuation handling. This work studies (in the setting of relational semantics) two new approaches to the polymorphic typing of these non-applicative features. The first one relies on a restriction of generalization over types (the notion of dangerous variables), and on a refined typing of functional values (closure typing). The resulting type system is compatible with the ML core language, and is the most expressive type systems for ML with imperative features proposed so far. The second approach relies on switching to ``by-name'' semantics for the constructs of polymorphism, instead of the usual ``by-value'' semantics. The resulting language differs from ML, but lends itself easily to polymorphic typing. Both approaches smoothly integrate non-applicative features and polymorphic typing.Le typage statique avec types polymorphes, comme dans le langage ML, s'adapte parfaitement aux langages purement applicatifs, leur apportant souplesse et expressivité. Mais il ne s'étend pas naturellement au trait principal des langages algorithmiques: la modification en place des structures de données. Des difficultés de typage similaires apparaissent avec d'autres extensions des langages applicatifs: les variables logiques, la communication inter-processus à travers des canaux, et la manipulation de continuations en tant que valeurs. Ce travail étudie, dans le cadre de la sémantique relationnelle, deux nouvelles approches du typage polymorphe de ces constructions non-applicatives. La première repose sur une restriction de l'opération de généralisation des types (la notion de variables dangereuses), et sur un typage plus fin des valeurs fonctionnelles (le typage des fermetures). Le système de types obtenu reste compatible avec le noyau applicatif de ML, et se révèle être le plus expressif parmi les systèmes de types pour ML plus traits impératifs proposés jusqu'ici. La seconde approche repose sur l'adoption d'une sémantique ``par nom'' pour les constructions du polymorphisme, au lieu de la sémantique ``par valeur'' usuelle. Le langage obtenu s'écarte de ML, mais se type très simplement avec du polymorphisme. Les deux approches rendent possible l'interaction sans heurts entre les traits non-applicatifs et le typage polymorphe