The Join-Calculus: a Calculus for Distributed Mobile Programming

This dissertation presents an elementary model of distributed programming, studies this model as a process calculus, and uses this model as the core of a programming language. The join calculus is a small calculus in which computation consists only of asynchronous message-passing communication. It can also be interpreted as the concurrent extension of a small functional language. Its operational semantics is given in terms of chemical abstract machines, with enough details to suggest an actual implementation. By construction, every reduction step can be implemented in at most one low-level network message, independently of the distribution of processes at run-time. We explore several refinements of the join calculus that give a more explicit account of distribution, including primitives for agent-based migration, partial failure, and failure detection. These refinements preserve global scopes and network transparency in the absence of failures. We use numerous notions of observational equivalences adapted to asynchronous systems. These equivalences are organized in a hierarchy where each tier corresponds to a trade-off between suitable discriminating power and efficient proof techniques. These equivalences and used to establish the correctness of encodings internal to the join-calculus and cross-encodings with the pi-calculus.