# topic.locality_typing.bib

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

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

@techreport{Sew97c,
author = {Peter Sewell},
title = {Global/Local Subtyping for a Distributed $\pi$-calculus},
institution = {Computer Laboratory, University of Cambridge},
year = {1997},
optkey = {},
opttype = {},
number = {UCAM-CL-TR-435},
month = aug,
note = {57pp. },
pdf = {http://www.cl.cam.ac.uk/~pes20/globallocal.ch.pdf},
ps = {http://www.cl.cam.ac.uk/~pes20/globallocal.ch.ps},
pscmr = {http://www.cl.cam.ac.uk/~pes20/globallocal.cmr.ps},
url = {http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-435.html},
abstract = {In the design of mobile agent programming languages there is a tension between the implementation cost and the expressiveness of the communication mechanisms provided. This paper gives a static type system for a distributed pi-calculus in which the input and output capabilities of channels may be either global or local. This allows compile-time optimization where possible but retains the expressiveness of channel communication. Subtyping allows all communications to be invoked uniformly. Recursive types and products are included. The distributed pi-calculus used integrates location and migration primitives from the Distributed Join Calculus with asynchronous pi communication, taking a simple reduction semantics. Some alternative calculi are discussed. },
topic = {locality_typing}
}

@inproceedings{Sew97d,
author = {Peter Sewell},
title = {Global/Local Subtyping and Capability Inference for a Distributed $\pi$-calculus},
conf = {ICALP 1998},
booktitle = {Proceedings of the 25th International Colloquium on Automata, Languages and Programming (Aalborg). LNCS 1443},
optcrossref = {},
optkey = {},
opteditor = {},
optvolume = {},
optnumber = {},
optseries = {},
year = {1998},
optorganization = {},
publisher = {Springer-Verlag},
This paper considers how locality restrictions on the use of capabilities can be enforced by a static type system. A distributed $\pi$-calculus with a simple reduction semantics is introduced, integrating location and migration primitives from the Distributed Join Calculus with asynchronous $\pi$ communication. It is given a type system in which the input and output capabilities of channels may be either global, local or absent. This allows compile-time optimization where possible but retains the expressiveness of channel communication. Subtyping allows all communications to be invoked uniformly. We show that the most local possible capabilities for internal channels can be inferred automatically.},