###
Nomadic
Pi Calculi: Expressing and Verifying Infrastructure for Mobile
Computation

Asis Unyapoth. Ph.D. Thesis.
Technical
Report 514, Computer Laboratory, University of Cambridge, June 2001.
#### 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.