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

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

                                   INRIA

             ==================================================
                       Effets cachés en style direct,
             ou: une règle d'anti-encadrement d'ordre supérieur
             ==================================================

La logique de séparation repose sur deux formes duales de modularité: le
"raisonnement local" rend une partie de l'état invisible à l'intérieur d'une
certaine portée statique, tandis que "l'état caché" rend au contraire une
partie de l'état invisible à l'extérieur d'une portée statique. Dans la
littérature récente, ces idiomes sont tous deux expliqués en termes d'une
règle d'encadrement d'ordre supérieur ("higher-order frame rule").

J'expliquerai pourquoi cette explication de "l'état caché" impose un style par
passage de continuations (CPS), et n'est donc pas satisfaisante en pratique.
Pour résoudre ce problème, je présenterai une règle d'anti-encadrement d'ordre
supérieur ("higher-order anti-frame rule"), qui permet de cacher un état local
en style direct. Je formaliserai cette règle dans le cadre d'un système de
types doté de capacités pour un langage de programmation à la ML, et
j'esquisserai une preuve syntaxique de sûreté du typage. Enfin, je présenterai
plusieurs applications de cette règle, afin d'en illustrer l'expressivité.