The Seal Calculus

The Seal Calculus is a process language for describing mobile computation. Threads and resources are tree structured; the nodes thereof correspond to agents, the units of mobility. The Calculus extends a it-calculus core with synchronous, objective mobility of agents over channels. This paper systematically compares all previous variants of Seal Calculus. We study their operational behaviour with labelled transition systems and bisimulations; by comparing the resulting algebraic theories we highlight the differences between these apparently similar approaches. This leads us to identify the dialect of Seal that is most amenable to operational reasoning and can form the basis of a distributed programming language. We propose type systems for characterising the communications in which an agent can engage. The type systems thus enforce a discipline of agent mobility, since the latter is coded in terms of higher-order communication. (c) 2005 Elsevier Inc. All rights reserved.