To: seminaire-gallium-moscova@inria.fr From: Francois.Pottier@inria.fr Subject: SEM - INRIA : Gallium - 11/02/08 - 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 Lundi 11 février, 10h30 ----------- Didier Rémy ----------- INRIA ============================== Une explication moderne de MLF ============================== MLF est un système de type qui généralise le Système F tout en permettant l'inférence de type comme dans le langage ML. Les types des paramètres de fonctions utilisés de façon monomorphe, toutes les abstractions et toutes applications de types sont inférés. Les paramètres de fonctions utilisées de façon polymorphe et seulement ceux-ci doivent être annotés. La première présentation de MLF, bien que relativement simple du point de vue de l'utilisateur, était difficile, peu modulaire et assez peu intuitive pour le concepteur. Dans cet exposé, je vous raconterai l'histoire de MLF dans sa version moderne, en utilisant une représentation graphique des types et m'appuyant sur une interprétation des types de MLF comme un ensemble de types du système F. Cette approche éclaire les faces cachées de la présentation d'origine, souligne bien mieux les liens étroits avec le système F et surtout avec le langage ML. Elle débouche également sur des algorithmes d'unification et d'inférence qui ont la même complexité que ceux de ML. NB: 1) Cet exposé s'appuie sur des travaux en collaboration avec Didier Le Botlan et Boris Yakobowski. 2) Cet exposé est une réplique de mon exposé au dernier Workshop ML.