To: seminaire-gallium-moscova@inria.fr
From: Francois.Pottier@inria.fr
Subject: SEM - INRIA : Gallium - 26/10/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 26 octobre, 10h30

                              ----------------
                              François Pottier
                              ----------------

                                   INRIA

                  =======================================
                  De ML à F_omega avec sortes récursives:
                    une traduction monadique bien typée
                  =======================================

La traduction monadique bien connue explicite le tas et le fait circuler à
travers les calculs sous forme d'un argument et résultat supplémentaires. Si
le langage de départ est doté de références et de fonctions de première
classe, comme c'est le cas en ML, alors il est particulièrement difficile de
comprendre de quel système de types on doit doter le langage cible pour
pouvoir argumenter que cette traduction produit des programmes bien typés. Je
présenterai une solution à ce problème, en choisissant pour langage cible une
version de F_omega dotée de certaines sortes récursives.