Nomadic pict: Programming languages, communication infrastructure overlays, and semantics for mobile computation

Pict project. We define two levels of abstraction as calculi with precise semantics: a low-level Nomadic π calculus with migration and location-dependent communication, and a high-level calculus that adds location-independent communication. Implementations of locationindependent communication, as overlay networks that track migrations and forward messages, can be expressed as translations of the high-level calculus into the low. We discuss the design space of such overlay network algorithms and define three precisely, as such translations. Based on the calculi, we design and implement the Nomadic Pict distributed programming language, to let such algorithms (and simple applications above them) to be quickly prototyped. We go on to develop the semantic theory of the Nomadic π calculi, proving correctness of one example overlay network. This requires novel equivalences and congruence results that take migration into account, and reasoning principles for agents that are temporarily im...

• Type: Journal
• Year: 2010
• Where: TOPLAS
• Authors: Peter Sewell, Pawel T. Wojciechowski, Asis Unyapoth
• Keywords: Design, Nomadic, Semantics, TOPLAS 2010