To: seminaire@pauillac.inria.fr
From: James.Leifer@inria.fr
Subject: SEM - INRIA : Moscova - 22/10/04 - 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
                           Amphi Turing du Bat 1.

                         Vendredi 22 octobre, 10h30

                                ------------
                                Peter Sewell
                                ------------

                Computer Laboratory, University of Cambridge

 =========================================================================
 Acute: high-level programming language design for distributed computation
 =========================================================================

Joint work with James Leifer, Keith Wansbrough, Mair Allen-Williams,
Francesco Zappa Nardelli, Pierre Habouzit, and Viktor Vafeiadis.

http://www.cl.cam.ac.uk/users/pes20/acute/index.html

In this talk I'll discuss the design space of high-level languages for
distributed computation, focussing on typing, naming, and version
change. We have designed, formally specified and implemented an
experimental language, Acute. This extends an OCaml core to support
distributed development, deployment, and execution, allowing type-safe
interaction between separately-built programs. It is expressive enough
to enable a wide variety of distributed infrastructure layers to be
written as simple library code above the byte-string network and
persistent store primitives, disentangling the language runtime from
communication.

This requires a synthesis of novel and existing features:

    * type-safe interaction between programs, with marshal and
       unmarshal primitives;
    * dynamic loading and controlled rebinding to local resources;
    * modules and abstract types with abstraction boundaries that are
       respected by interaction;
    * global names, generated either freshly or based on module
       hashes: at the type level, as runtime names for abstract types;
       and at the term level, as channel names and other interaction
       handles;
    * versions and version constraints, integrated with type identity;
    * local concurrency and thread thunkification; and
    * second-order polymorphism with a namecase construct.

The implementation is above FreshOCaml.  The language design deals
with the interplay among these features and the core. The semantic
definition tracks abstraction boundaries, global names, and hashes
throughout compilation and execution, but still admits an efficient
implementation strategy.