Hostname: page-component-6bf8c574d5-b4m5d Total loading time: 0 Render date: 2025-02-21T04:07:33.561Z Has data issue: false hasContentIssue false

Equational properties of mobile ambients

Published online by Cambridge University Press:  20 May 2003

ANDREW D. GORDON
Affiliation:
Microsoft Research Ltd., 7 J. J. Thompson Avenue, Cambridge CB3 0FB, United Kingdom
LUCA CARDELLI
Affiliation:
Microsoft Research Ltd., 7 J. J. Thompson Avenue, Cambridge CB3 0FB, United Kingdom
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

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.

Type
Research Article
Copyright
2003 Cambridge University Press