To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 20/04/07 - Paris - FR Vous pouvez vous abonner à nos annonces de séminaires http://pauillac.inria.fr/seminaires/ S E M I N A I R E __ / _` _ / / o /| /| __ __ __ __ _ _ / ) __) / / / / / /\/| ----- / |/ | / )(_ / / ) ) ) __) (___/ (_/ (_ (_ / (__/ / | / | (__/ __)(_ (__/ (_/ (_/ I N R I A - Rocquencourt Amphi Turing du bâtiment 1 Vendredi 20 avril, 10h30 ------------------------------------- Jérôme Vouillon et Paul-André Melliès ------------------------------------- CNRS ========================================================= Types polymorphes et récursifs dans un cadre opérationnel ========================================================= Nous expliquerons lors de cet exposé comment construire un modèle de réalisabilité des types polymorphes et récursifs, en partant d'un langage non typé de termes et de contextes. Une relation d'orthogonalité indique quand un terme et un contexte peuvent être combinés sans provoquer d'erreurs à l'exécution. Les types sont interprétés comme des ensembles de termes fermés par bi-orthogonalité. Notre résultat principal est que les types récursifs sont approximés par des suites convergentes de types intervalles. La démonstration de ce résultat s'appuie sur une stratification des termes induite par les types, et non plus par la syntaxe elle-même, comme dans les techniques usuelles héritées des travaux de MacQueen, Plotkin et Sethi sur le modèle idéal. De la sorte, nous gardons le langage élémentaire (un lambda-calcul en appel par nom) et non stratifié (pas de tests dynamiques de type). Nous expliquerons aussi brièvement comment intégrer la paramétricité dans ce cadre, en partant d'une relation d'orthogonalité entre paires de termes et de contextes.