To: seminaire@pauillac.inria.fr
From: Didier.Remy@inria.fr
Subject: SEM - INRIA : Mosvova - 11/07/03 - Paris - FR

      Vous pouvez maintenant vous abonner à nos annonces de séminaires
             http://pauillac.inria.fr/seminaires/subscribe.html


                             S E M I N A I R E
                                         . ___ 
                           /   _   _      /   _   /
                          /   / \ / \  / /   __| /
                         |___ |_/ |_/ / |__ |_/ |_
       ___      .                  /    
      /    ___   __  /_  _   /   _/        /| /|  _   __ __ _       _ 
     /    /   / /_  /   __| /             / |/ | / \ /_ /  / \ | / __|
    |___ /   / __/ |_  |_/ |_            /     | |_/__/ |_ |_/ |/ |_/
                                                
                          I N R I A - Rocquencourt
                        Salle de conférence du Bat 8

                         Vendredi 11 juillet, 10h30

                               --------------
                               Gilles Peskine
                               --------------


                ===========================================
                Types abstraits et programmation distribuée
                ===========================================

        (Travail en commun avec James Leifer, en collaboration avec
        Peter Sewell et Keith Wansbrough (University of Cambridge))

   L'abstraction de types est un trait essentiel des langages de la famille
   ML pour écrire les logiciels de taille importante.  La sérialisation est
   un   ingrédient   indispensable  des   programmes   distribués,  de   la
   transmission  de valeurs  sur un  réseau, et  du stockage  persistant de
   données.  Dans cet  exposé, nous combinons les deux,  en développant des
   sémantiques statique  et dynamique de la  sérialisation qui garantissent
   la sûreté des abstractions entre des programmes développés séparément.

   Nous  obtenons un espace  de nommage  pour les  types abstraits  qui est
   global,  c'est-à-dire commun  à  tous les  programmes,  par hachage  des
   déclarations de modules. Nous  examinons des scénarios dans lesquels des
   valeurs de  types abstraits sont transmises entre  les programmes ; nous
   garantissons que  les notions statique  et dynamique d'égalité  de types
   coïncident  grâce à  la construction  de la  fonction de  hachage.  Nous
   utilisons les « singleton kinds » pour exprimer les abstractions dans la
   sémantique statique ; ces  abstractions sont suivies à la  trace par des
   crochets colorés dans la sémantique dynamique. Cette méthode nous permet
   de  prouver   les  théorèmes   de  préservation,  d'effacement,   et  de
   correspondance.  Nous  proposons cette  technique  comme  une base  pour
   étendre  les langages  à la  ML, car  elle est  simple et  pratique pour
   l'utilisateur comme pour l'implémenteur.