# Basic Calculi

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/.

## Our results

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

## Publications

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:

*Handbook of Pocess Algebra*, pp 479-543, Elsevier, 2001.

*Proc. 21st Symposium on Logic In Computer Science: LICS 2006*, pp 59-68, IEEE, Piscataway, NJ, 2006. (DOI).

*Proceedings of CALCO 2005*, 2005. (DOI, External link).

*Proc. 7th Workshop on Coalgebraic Methods in Computer Science*, volume 106 of Electronic Notes in Theoretical Computer Science, pp 105-120, Elsevier, 2004. (DOI).

*Mathematical Structures in Computer Science*, volume 13, number 5, pp 657-683, 2003. (DOI).

*Proof, Language and Interaction, Essays in Honor of Robin Milner*, pp 621-637, MIT Press, 2000.

*Proceedings of ICALP'98*, volume 1443 of Lectute notes in computer science, pp 455-469, Springer, Berlin, 1998. (DOI).

*Proceedings of LICS'98*, Proceedings / Symposium on Logic in Computer Science, pp 176-185, IEEE Computer Society, Los Alamitos, CA, 1998. (DOI).

*Information and Computation*, volume 120, number 2, pp 174-197, 1995. (DOI).

*Nordic Journal of Computing*, volume 2, number 4, pp 407-443, 1995.

*Proceedings of CAV'94*, pp 428-440, 1994. (DOI).

*Theoretical Computer Science*, volume 114, number 1, pp 149-171, 1993. (DOI).

*Information and Computation*, volume 100, number 1, pp 1-40, 1992. (DOI).

*Information and Computation*, volume 100, number 1, pp 41-77, 1992. (DOI).

*Formal Aspects of Computing*, volume 4, number 6, pp 497-543, 1992. (DOI).