[TYPES] Paper: Acute - high-level programming language design for distributed computation

[Peter Sewell]

Dear All,

We would like to announce the papers

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

 * Acute: high-level programming language design for distributed
   computation. Design rationale and language definition

which are available from

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

together with some example Acute code.  The first paper gives an
overview of the main design choices; the second contains an extended
design discussion, an introduction to the semantics, examples
illustrating the semantics, and the full language definition.


This work explores 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, which 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 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.


The Acute team: Peter Sewell, James J. Leifer, Keith Wansbrough, Mair
Allen-Williams, Francesco Zappa Nardelli, Pierre Habouzit, and Viktor
Vafeiadis.