Towards a lambda-calculus for concurrent and communicating systems

Abstract

We introduce a calculus for concurrent and communicating processes, which is a direct and simple extension of the λ-calculus. The communication mechanism we use is that of Milner's calculus CCS: to communicate consists in synchronously sending and receiving a value through a shared port. Then the calculus is parameterized on a given set of port names, which are used in the two primitives for sending and receiving a value — as in the λ-calculus, a value can be any term. We use two parallel constructs: the first is interleaving, which does not allow communication between agents. The second, called cooperation, is a synchronizing construct which forces two agents to communicate on every port name. We show that the λ-calculus is a simple sub-calculus of ours: λ-abstraction is a particular case of reception (on a port named λ), and application is a particular case of cooperation.