[no subject]

[Peter Sewell <Peter.Sewell@xxxxxxxxxxxx>]

Dear All,

I'm pleased to announce that Asis Unyapoth's PhD thesis

  Nomadic Pi Calculi: Expressing and Verifying Infrastructure for
    Mobile Computation

is available electronically from

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

together with other papers on Nomadic Pi(ct).  The abstract is
below. See http://www.ftp.cl.cam.ac.uk/ftp/papers/reports/ for how to
obtain a hard copy.

Peter



Abstract

This thesis addresses the problem of verifying distributed
infrastructure for mobile computation. In particular, we study
language primitives for communication between mobile agents. They can
be classified into two groups. At a low level there are location
dependent primitives that require a programmer to know the current
site of a mobile agent in order to communicate with it. At a high
level there are location independent primitives that allow
communication with a mobile agent irrespective of any
migrations. Implementation of the high level requires delicate
distributed infrastructure algorithms. In earlier work of Sewell,
Wojciechowski and Pierce, the two levels were made precise as process
calculi, allowing such algorithms to be expressed as encodings of the
high level into the low level; a distributed programming language
Nomadic Pict has been built for experimenting with such encodings.

This thesis turns to semantics, giving a definition of the core
language (with a type system) and proving correctness of an example
infrastructure. This involves extending the standard semantics and
proof techniques of process calculi to deal with the new notions of
sites and agents. The techniques adopted include labelled transition
semantics, operational equivalences and preorders (\eg. expansion and
coupled simulation), ``up to'' equivalences, and uniform
receptiveness. We also develop two novel proof techniques for
capturing the design intuitions regarding mobile agents: we consider
translocating versions of operational equivalences that take migration
into account, allowing compositional reasoning; and temporary
immobility, which captures the intuition that while an agent is
waiting for a lock somewhere in the system, it will not migrate.

The correctness proof of an example infrastructure is non-trivial. It
involves analysing the possible reachable states of the encoding
applied to an arbitrary high-level source program. We introduce an
intermediate language for factoring out as many `house-keeping'
reduction steps as possible, and focusing on the partially-committed
steps.


  
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
The "models for mobility" mailing list     mailto:moca@xxxxxxxxxxxxxxx
 http://www-sop.inria.fr/mimosa/personnel/Davide.Sangiorgi/moca.html