The -Calculus: Notes on Labelled Semantics

Paola Quaglia

December 1998

Abstract:

The -calculus is a name-passing calculus that allows the description of distributed systems with a dynamically changing interconnection topology. Name communication, together with the possibility of declaring and exporting local names, gives the calculus a great expressive power. For instance, it was remarkably shown that process-passing calculi, that express mobility at higher order, can be naturally encoded in -calculus.

Since its very first definition, the -calculus proliferated in a family of calculi slightly departing the one another either in the communication paradigm (polyadic vs monadic, asynchronous vs synchronous) or in the bisimulation semantics (labelled vs unlabelled, late vs early vs open vs barbed vs ...).

These short notes present a collection of the labelled strong semantics of the (synchronous monadic) -calculus. The notes could not possibly substitute any of the standard references listed in the Bibliography. They rather represent an attempt to group together, using a uniform notation and the terminology that got assessed over the last years, a few definitions and concepts otherwise scattered throughout the -calculus literature.

Contents

1

Preliminaries

2

Syntax

3

Labelled semantics

3.1

Late semantics

3.2

Early semantics

3.3

Open semantics

Available as PostScript, PDF, DVI.