Microsoft Research
This approach has led to major progress in software composability and reliability. Unfortunately, it is based on a number of assumptions that simply do not hold on modern wide area networks. There, access to resources is intrinsically unreliable (because of failures, congestion, and voluntary disconnected operation) and not transparent (because of variations in latency and bandwidth, hardware and software mobility, and the presence of firewalls). Moreover, the network itself is not a given entity: it is dynamic, not centrally managed, sometimes self-organizing, and must be discovered (and rediscovered) during the computation process.
We discuss the new challenges of computation on wide area networks, and introduce a formalism, the Ambient Calculus, that matches some fundamental characteristics of these networks. Our approach reflects the intuition that, to function satisfactorily on wide area networks, systems must be partitioned along security boundaries, and made hierarchical, internally mobile, and secure.
The Ambient Calculus is a process calculus that takes (process) mobility, instead of communication, as the primitive notion, and where mobility is subject to security constraints. From a formal point of view, we develop a simple but computationally powerful calculus that is sufficient to directly express notions such as "securely crossing a firewall". We develop an operational semantics (with some variations), and related proof techniques, type systems, and logics for temporal and spatial properties of mobile systems.
Much of this material reflects joint work with Andrew D. Gordon.