To: seminaire@pauillac.inria.fr
From: Didier.Remy@inria.fr
Subject: SEM - INRIA : Cristal - 21/06/02 - 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 conference du Bat 58 <====== ATTENTION !

                          Vendredi 21 juin, 10h30

                               -------------
                               Eugenio Moggi
                               -------------


        ============================================================
        Higher-Order Types and Meta-Programming for Global Computing
        ============================================================


  The  talk presents  MetaKlaim, a  case  study in  modeling the  spatial,
  temporal and security aspects necessary for global computing.  MetaKlaim
  integrates MetaML (an extension  of SML for multi-stage programming) and
  Klaim (a Kernel Language for  Agents Interaction and Mobility), in order
  to allow interleaving of  meta-programming activities (like assembly and
  linking  of  code fragments),  security  checks  (like type-checking  at
  administrative boundaries) and normal computational activities.

  The staging  annotations of MetaML  provide a fine-grain control  of the
  temporal aspects,  Klaim's primitives support  location awareness, while
  the type  system supports security through  the use of  global types (in
  combination with dynamic type-checking)  and generic mobile code through
  the use of polymorphism (a la system F).

  The  talk describes  syntax, type  system and  operational  semantics of
  MetaKlaim, states two  type safety results, and exemplifies  its use for
  describing mobile code applications.

  PS: joint work with G. Ferrari and R. Pugliese