Mobility Types for Mobile Ambients

An ambient is a named cluster of processes and subambients, which moves as a group. The untyped ambient calculus is a process calculus in which ambients model a variety of concepts such as network nodes, packets, channels, and software agents. In these models, some ambients are intended to be mobile, some immobile; and some are intended to be ephemeral, some persistent. We describe type systems able to formalize these intentions: they can guarantee that an ambient will remain immobile, and that an ambient will not be dissolved by its environment. These guarantees could help establish security properties of models, for instance. A novel feature of our type systems is their distinction between mobile and immobile processes.