Implementation and Semantics of Mobile Agent Infrastructure
The Nomadic Pict project studied programming language design and
communication primitives for mobile computation.
Communication primitives for interaction between
mobile agents can be classified into two levels of abstraction. At a low level
there are location dependent primitives that require an
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 its current site and of any migrations.
Implementation of these requires delicate distributed infrastructure.
We proposed a simple calculus of agents that allows implementations
of such distributed infrastructure algorithms to be expressed as encodings,
or compilations, of the whole calculus into the fragment with only
location dependent communication.
These encodings give executable descriptions of the algorithms,
providing a clean implementation strategy for prototype languages.
The calculus is equipped with a precise semantics, providing a solid
basis for understanding the algorithms and for reasoning about
their correctness and robustness.
We implemented a language, Nomadic Pict, based on the calculus
to enable experiments with
and agent computing. Nomadic Pict is an extension of Pict with the notion of
agents, migration, distribution, and failures.
At the same time we developed reasoning techniques for
correctness and robustness proofs of these algorithms.
Those involved include
An alpha release of the
implementation is available from the
web page. It includes a tutorial.
Some relevant papers are below; others can be found on the individual
Nomadic Pict: Programming Languages, Communication Infrastructure Overlays, and
Semantics for Mobile Computation. Sewell, Wojciechowski, and
Unyapoth. In TOPLAS 2010 32(4).
Verifying Overlay Networks for Relocatable Computations
(or: Nomadic Pict, relocated). Sewell and Wojciechowski. Position
paper for the MSR/HP Labs research meeting on
The Rise and Rise of the Declarative Datacentre, May 2008.
Pi Calculi: Expressing and Verifying Infrastructure for Mobile Computation,
Ph.D. thesis. Appeared as Technical
Report 514, Computer Laboratory, University of Cambridge, June 2001.
Here is the
for Location-Independent Communication between Mobile
Agents. Pawel Wojciechowski. Technical
Report 2001/13, Communication Systems Department, EPFL, March 2001. Abstract.
In pdf. Here
is a shorter version
which appeared in the AISB'01
on Software mobility and adaptive behaviour.
These are copied in Cambridge:
Nomadic Pict: Correct Communication
Infrastructure for Mobile Computation,
Asis Unypoth and Peter Sewell.
In POPL 2001.
Also in pdf,
dvi, and ps.
Pict: Language and Infrastructure Design for Mobile Computation .
Pawel Wojciechowski, Ph.D. thesis. Appeared as Technical
Report 492, Computer Laboratory, University of Cambridge, June 2000.
Also in pdf. Here
is the abstract
These are copied in Cambridge:
Nomadic Pict: Language
Infrastructure Design for Mobile Agents,
Pawel Wojciechowski and Peter Sewell.
This appeared in
ASA/MA'99 (First International Symposium on Agent
Systems and Applications/Third International Symposium on
Mobile Agents), October 1999.
An extended version appeared in IEEE Concurrency vol 8 no 2, 2000.
Location-Independent Communication for Mobile
Agents: a Two-Level Architecture, Peter Sewell, Pawel Wojciechowski and Benjamin Pierce.
Technical Report 462, Computer Laboratory, University of Cambridge.
A version of this appeared in Internet Programming Languages, LNCS 1686.
Location Independence for Mobile Agents,
Peter Sewell, Pawel Wojciechowski and Benjamin Pierce.
This appeared in the
Workshop on Internet Programming Languages, 1998. It is largely
superseded by Technical Report 462 above.
[Validate this page.]