To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 09/02/09 - 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 9 février, 10h30

                              ----------------
                              Boris Yakobowski
                              ----------------

                         CNRS - Université Paris 7

                   ======================================
                   xMLF : un langage à la Church pour MLF
                   ======================================

Le langage MLF combine l'inférence de types à la ML avec l'expressivité des
types du second ordre du Système F. Pour cela, il introduit des types plus
riches que ceux du Système F. Cela pose problème lorsque MLF doit être
utilisé dans un compilateur dont les langages intermédiaires sont typés : le
Système F, qui est strictement moins expressif que MLF, ne peut plus être
utilisé comme langage cible.

Dans cet exposé je présenterai xMLF, une version à la Church de MLF. Dans
xMLF, toutes les informations de types (abstractions et applications) sont
totalement explicites.  En particulier, l'instance sur les types est rendue
explicite par des témoins de calculs, qui peuvent être réduits par des
règles appropriées.  Je montrerai que xMLF est correct pour les stratégies
d'appel par nom, d'appel par valeur (avec value restriction ou non), et que
la réduction forte est confluente.  Dans un deuxième temps, je montrerai
comment traduire le résultat de l'inférence (pour la présentation graphique
de xMLF) en un terme xMLF bien typé.  Enfin, je discuterai de la différence
d'expressivité entre xMLF et les autres présentations de MLF.