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 ...

• Type: Conference
• Year: 2001
• Where: POPL
• Authors: Asis Unyapoth, Peter Sewell
• Keywords: Delicate Distributed Infrastructure, Location Dependent Primitives, Location Independent Primitives, POPL 2001, Programming Languages