Nomadic pict: correct communication infrastructure for mobile computation

14 years 7 months ago
Nomadic pict: correct communication infrastructure for mobile computation
This paper addresses the design and verification of 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 with Wojciechowski and Pierce we made the two levels precise as process calculi, allowing such algorithms to be expressed as encodings of the high level into the low level; we built Nomadic Pict, a distributed programming language for experimenting with such encodings. In this paper we turn to semantics, giving a definition of the core language and proving correctness of an example ...
Asis Unyapoth, Peter Sewell
Added 03 Dec 2009
Updated 03 Dec 2009
Type Conference
Year 2001
Where POPL
Authors Asis Unyapoth, Peter Sewell
Comments (0)