@comment{{This file has been generated by bib2bib 1.96}}

@comment{{Command line: /usr/bin/bib2bib -c topic:"nomadic_pict" -ob topic.nomadic_pict.bib sewellbib2.bib}}

@inproceedings{SWP98,
author = {Peter Sewell and Pawe{\l} T. Wojciechowski
and  Benjamin C. Pierce},
title = {Location Independence for Mobile Agents},
conf = {WIPL 1998},
booktitle = {Proceedings of the Workshop on Internet Programming Languages (Chicago), in conjunction with ICCL},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {1998},
optorganization = {},
optpublisher = {},
month = may,
note = {6pp},
optpages = {6pp},
optnote = {},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/users/pes20/lima-draft.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/lima-draft.ps},
workshopurl = {http://www.math.luc.edu/iccl98/ipl-cfp.html},
}

@techreport{SWP99a,
author = {Peter Sewell and Pawe{\l} T. Wojciechowski
and  Benjamin C. Pierce},
title = {Location-Independent Communication for Mobile Agents: a Two-Level Architecture},
institution = {Computer Laboratory, University of Cambridge},
year = {1999},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-462},
month = apr,
note = {31pp. },
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/wipl-tr.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/wipl-tr.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-462.html},
abstract = {We study communication primitives for interaction 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 its current site and of any migrations. Implementation of these requires delicate distributed infrastructure. We propose a simple calculus of agents that allows implementation 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 reasoning about their correctness and robustness. Two sample infrastructure algorithms are presented as encodings.},
}

@inproceedings{WS99,
author = {Pawe{\l} T. Wojciechowski and Peter Sewell},
title = {{N}omadic {P}ict: Language and Infrastructure Design for Mobile Agents},
conf = {ASA/MA 1999},
booktitle = {Proceedings of First International Symposium on Agent Systems and Applications/Third International Symposium on Mobile Agents (Palm Springs)},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {1999},
optorganization = {},
optpublisher = {},
month = oct,
pages = {2--12},
note = {Best paper award. },
optannote = {},
url = {https://doi.org/10.1109/ASAMA.1999.805388},
doi = {10.1109/ASAMA.1999.805388},
pdf = {http://www.cl.cam.ac.uk/users/pes20/asama.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/asama.ps},
abstract = {We study the distributed infrastructures required for
location-independent communication between migrating
agents. These infrastructures are problematic: different applications may have very different patterns of migration and
communication, and require different performance and robustness properties; algorithms must be designed with these
in mind. To study this problem we introduce an agent programming language --- Nomadic Pict. It is designed to allow
infrastructure algorithms to be expressed as clearly as possible, as translations from a high-level language to a low
level. The levels are based on rigorously-defined process
calculi, they provide sharp levels of abstraction. In this paper we describe the language and use it to develop an infrastructure for an example application. The language and
examples have been implemented; we conclude with a description of the compiler and runtime.
},
}

@inbook{SWP99b,
author = {Peter Sewell and Pawe{\l} T. Wojciechowski
and  Benjamin C. Pierce},
title = {Location-Independent Communication for Mobile Agents: a Two-Level Architecture},
booktitle = {Internet Programming Languages, LNCS 1686},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {1999},
optorganization = {},
publisher = {Springer-Verlag},
month = oct,
pages = {1--31},
note = {},
optannote = {},
opturl = {https://doi.org/10.1007/3-540-47959-7_1},
doi = {10.1007/3-540-47959-7_1},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-462.html},
pdf = {http://www.cl.cam.ac.uk/~pes20/wipl-tr.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/wipl-tr.ps},
abstract = {We study communication primitives for interaction 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 its current site and of any migrations. Implementation of these requires delicate distributed infrastructure. We propose a simple calculus of agents that allows implementation 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 reasoning about their correctness and robustness. Two sample infrastructure algorithms are presented as encodings.},
}

@article{WS00,
author = {Pawe{\l} T. Wojciechowski and Peter Sewell},
title = {{N}omadic {P}ict: Language and Infrastructure Design for Mobile Agents},
journal = {{IEEE} {C}oncurrency},
year = {2000},
optkey = {},
volume = {8},
number = {2},
month = {April--June},
pages = {42--52},
note = {Invited submission for ASA/MA 99. },
url = {https://doi.org/10.1109/4434.846193},
doi = {10.1109/4434.846193},
optannote = {},
abstract = {Location-independent communication between migrating agents requires a distributed infrastructure. The authors describe their Nomadic Pict distributed programming language and use it to develop an infrastructure for an example application.},
}

@inproceedings{US01,
author = {Asis Unyapoth and Peter Sewell},
title = {Nomadic {P}ict: Correct Communication Infrastructure for Mobile Computation},
conf = {POPL 2001},
booktitle = {Proceedings of the 28th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (London)},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {2001},
optorganization = {},
optpublisher = {},
month = jan,
pages = {116--127},
note = {},
optannote = {},
url = {http://doi.acm.org/10.1145/360204.360214},
doi = {10.1145/360204.360214},
pdf = {http://www.cl.cam.ac.uk/users/pes20/nproofs-popl.pdf},
ps = {http://www.cl.cam.ac.uk/users/pes20/nproofs-popl.ps},
abstract = {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 infrastructure. This requires novel techniques:
we develop equivalences that take migration into account,
and reasoning principles for agents that are temporarily immobile (eg. waiting on
a lock elsewhere in the system).
},
}

@inproceedings{npict-r2d2,
author = {Peter Sewell and Pawe{\l} Wojciechowski},
title = {Verifying Overlay Networks for Relocatable Computations
optcrossref = {},
optkey = {},
conf = {RRDD Workshop, 2008},
booktitle = {Proceedings of the workshop on The Rise and Rise of the Declarative Datacentre, Microsoft Research Technical Report MSR-TR-2008-61},
pages = {43--46},
year = {2008},
opteditor = {Karthikeyan Bhargavan, Andrew Gordon, Tim Harris, and Peter Toft},
optvolume = {},
optnumber = {},
optseries = {},
month = may,
optorganization = {},
optpublisher = {},
optnote = {},
optannote = {},
pdf = {http://www.cl.cam.ac.uk/~pes20/r2d2.pdf},
abstract = {In the late 1990s we developed a calculus, Nomadic Pict, in which
to express and verify overlay networks, for reliable communication
between relocatable computations. Then, efficient system support
for relocation was rare, and the calculus was reified in a prototype
high-level programming language. Now, relocatable computation
is a pervasive reality, though at the level of virtual machines rather
than high-level languages. One can ask whether the semantic theory
and algorithms developed for Nomadic Pict can be applied (or
adapted) to infrastructure for communication between these virtual
machines.},
}

@article{npict-toplas,
author = {Peter Sewell and Pawe{\l} Wojciechowski and Asis Unyapoth},
title = {Nomadic {Pict}: Programming Languages, Communication Infrastructure Overlays, and Semantics for Mobile Computation},
journal = {ACM Transactions on Programming Languages and Systems (TOPLAS)},
year = {2010},
optkey = {},
volume = {32},
number = {4},
pages = {1--63 (and electronic appendix, 33pp)},
optmonth = {},
optnote = {(Accepted for publication, 3 Sep.~2009)},
optannote = {},
doi = {10.1145/1734206.1734209},
pdf = {http://www.cl.cam.ac.uk/~pes20/npict.pdf},
abstract = {
Mobile computation, in which executing computations can move from one physical computing device to another, is a recurring theme: from OS process migration, to language-level mobility, to virtual machine migration. This article reports on the design, implementation, and verification of overlay networks to support reliable communication between migrating computations, in the Nomadic Pict project. We define two levels of abstraction as calculi with precise semantics: a low-level Nomadic $\pi$ calculus with migration and location-dependent communication, and a high-level calculus that adds location-independent communication. Implementations of location-independent 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 $\pi$ 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 immobile (e.g., waiting on a lock elsewhere in the system). The whole stands as a demonstration of the use of principled semantics to address challenging system design problems.
},