Equational Properties of Mobile Ambients
- Andy Gordon ,
- Luca Cardelli
FoSSaCS 1999 International Conference on Foundations of Software Science and Computation Structure |
Published by Springer, Berlin, Heidelberg
A shortened version of this paper appears in the proceedings of the conference on Foundations of Software Science and Computation Structures, Amsterdam, the Netherlands, 22 - 26 March 1999. The proceedings is published by Springer Verlag as a volume of the series Lecture Notes in Computer Science.
The ambient calculus is a process calculus for describing mobile computation. We develop a theory of Morris-style contextual equivalence for proving properties of mobile ambients. We prove a context lemma that allows derivation of contextual equivalences by considering contexts of a particular limited form, rather than all arbitrary contexts. We give an activity lemma that characterises the possible interactions between a process and a context. We prove several examples of contextual equivalence. The proofs depend on characterising reductions in the ambient calculus in terms of a labelled transition system.