Newsgroups: fr.announce.seminaires
Distribution: fr
To: fr-sem@frmug.org
From: Didier.Remy@inria.COUPER-CECI.fr
Organization: INRIA-Rocquencourt
Subject: SEM - INRIA : Mosvova - 21/04/00 - Paris - FR

***** Rectificatif: Le séminaire est programmé à 14 heures *****

           http://pauillac.inria.fr/bin/calendar/Seminaires


                             S E M I N A I R E

   ____              ____    .                   
  /   _   _        /    ___   __  /_  _   /     /| /|  _   __ __ _       _ 
 /   / \ / \  _   /    /   / /_  /   __| /  _  / |/ | / \ /_ /  / \ | / __|
|___ |_/ |_/     |___ /   / __/ |_  |_/ |_    /     | |_/__/ |_ |_/ |/ |_/
          /                                                                 
         /                                                                  
                          I N R I A - Rocquencourt, 
                       Salle de conference du Bat 11

                          Vendredi 21 avril, 14h00

                             -----------------
                             Silvano Dal-Zilio
                             -----------------

                       Microsoft Research (Cambridge)

           ======================================================
           Modélisation des régions dans un pi-calcul avec groupe
           ======================================================

    Dans  cet exposé,  nous  portons un  nouveau  regard sur  le calcul  des
    régions de Tofte et Talpin en  nous aidant d'un codage dans un pi-calcul
    typé avec groupes.

    Dans un langage fonctionnel ave  régions, les valeurs sont allouées dans
    des segments  mémoires déterminées à  la compilation. Ces  segments sont
    contrôlés  suivant une politique  de pile  qui améliore  sensiblement la
    gestion de la mémoire.  Ainsi, le  calcul des régions a été utilisé avec
    succès  comme langage  intermédiaire dans  l'implantation de  ML-Kit, un
    compilateur sans ramasse-miettes pour Standard ML.

    La notion de  groupes a été introduite dans le  calcul des ambients typé
    de Cardelli, Ghelli, et Gordon.  Dans ce calcul, comme dans le pi-calcul
    que nous  nous proposons d'utiliser,  chaque nom appartient à  un groupe
    statiquement déterminé.   Utilisé dans un système de  types avec effets,
    les groupes  permettent la vérification de certaines  propriétés liées à
    la mobilité.

    Notre  codage  précise  la  correspondance intuitive  entre  régions  et
    groupes.  Nous  proposons, entre autre,  une nouvelle formulation  de la
    propriété de  conservation du typage  pour le calcul des  régions. Notre
    codage  nous permet aussi  de prouver  la correction  de la  gestion des
    régions.   Ce  résultat  est   prouvé  à   l'aide  d'une   nouvelle  loi
    d'équivalence comportementale pour notre pi-calcul.