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

                             ------------------
                             Arthur Charguéraud
                             ------------------

                              ENS Lyon & INRIA

      ================================================================
      Traduction de programmes impératifs vers un langage fonctionnel
      à l'aide d'un système de types à base de capacités et de régions
      ================================================================

Nous montrerons comment un système de typage à base de capacités 
et de régions permet de structurer statiquement l'état mémoire,
et ce de manière relativement fine. Nous verrons alors que les 
dérivations de typage de notre système peuvent être utilisées pour
traduire des sources impératifs vers un langage purement 
fonctionnel. Ainsi, nous réduisons le problème de certification 
de programmes (bien typés) impératifs au problème de certification 
de programmes fonctionnels.