Much of the effort of the group has been in the area of the pi-calculus, a calculus of communicating systems in which one can naturally express processes which have changing structure. Not only may the component agents of a system be arbitrarily linked, but a communication between neighbours may change that linkage by passing the name of a communication link. The pi-calculus was developed by Milner, Parrow and Walker in the late 1980s.
The mechanism of name-passing, in combination with the paradigm of static binding (the scope of names may be dynamically extended by means of communication to include the receiver) has turned out to e.g.
- be surprisingly expressive for a vast variety of programming idioms (abstract data types, lambda-calculus, i.e. functional programming, object-oriented programming, imperative programming, logic and concurrent constraint programming, primitives for encryption/decryption);
- raise many interesting theoretical issues, e.g:
- the role of substitution for the observational semantics of communication by name-passing, giving rise to variants known as ground, early, late, open, and hyper, which often do not coincide,
- the proliferation and axiomatization of the various bisimulation, testing, and other process equivalences and congruences, ranging over the different styles of substitutions in the semantics,
- the study of individual operators (e.g. replication, bound output, delayed input, mis-/matching, choice, explicit substitution) w.r.t. expressiveness, implementability and combinatory counterparts,
- different modes of communication, e.g. synchronous, asynchronous, persistent, linear,
- mobility-specific aspects in non-interleaving semantics,
- the search for appropriate notions of modal and temporal logics,
- denotational models and their categorical interpretation,
- rich notions of type systems for processes, both inherited from sequential (functional) programming notions, like arrays, records, subtypes, linear and polymorphic types, as well as original notions of type, like mutex (semaphor-like) and graphical notions and the distinction between local and remote channels;
- provide solid foundations for the design of high-level concurrent and distributed programming languages (e.g. Pict, Facile, Join, TyCO, HACL, and Oz) that are also suited as scripting languages for mobile agents;
- allow for applications in the range of mobile (and standard) telecommunication protocols, as well as cryptographic protocols;
- trigger a whole family of related calculi: spi, join, fusion, update, blue, to mention just some
A web site with introductory material, bibliographies, links to researchers and groups in the field, related calculi and tools, can be found at http://lampwww.epfl.ch/mobility/.
In addition to the original development of the pi-calculus, its operational semantics, late/early semantics, etc, we have also (co-)developed
- modal logics for the pi-calculus; algebraic verification of telecom protocols; axiomatizations of early and late bisimulation equivalences
- an automated tool for equivalence checking, deadlock search, interactive simulation, sort inference, and model checking for the pi-calculus, and equivalence checking for the fusion calculus (below).
- graphical formalisms for the pi-calculus and for the solos calculus (below)
- the fusion calculus, a simplification of the pi-calculus with significantly extended expressiveness, and the solos calculus, a further simplification of the fusion calculus
- expressiveness studies:
- encodings of basic calculi for concurrent constraints (in pi and in fusion), and of the strong lambda-calculus in fusion
- encoding the full pi-calculus in the "trio" fragment
- encoding the full fusion calculus (and pi) in the solos calculus, where sequentiality is not primitive
- relating linear and persistent fragments of the asynchronous pi-calculus
- coalgebraic models of pi and fusion
There is a searchable bibliography on calculi for mobile processes on the net co-maintained by us, containing over 500 references from 1989-2002.
Selected publications by our group in this area: