Basic Calculi

pi.png 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:

An introduction to the pi-calculus. Joachim Parrow. In Handbook of Pocess Algebra, pp 479-543, Elsevier, 2001.

On the Expressiveness of Linearity vs Persistence in the Asynchronous Pi-Calculus. Catuscia Palamidessi, Vijay Saraswat, Frank D. Valencia, and Björn Victor. In Proc. 21st Symposium on Logic In Computer Science: LICS 2006, pp 59-68, IEEE, Piscataway, NJ, 2006. (DOI).
A Unifying Model of Variables and Names. Marino Miculan and Kidane Yemane. In Proceedings of FoSSaCS 2005, 2005. (DOI).
Modelling and Minimising the Fusion Calculus using HD-automata. Gianluigi Ferrari, Ugo Montanari, Emilio Tuosto, Björn Victor, and Kidane Yemane. In Proceedings of CALCO 2005, 2005. (DOI, External link).
Relationally Staged Computations in Calculi of Mobile Processes. Neil Ghani, Kidane Yemane, and Björn Victor. In Proc. 7th Workshop on Coalgebraic Methods in Computer Science, volume 106 of Electronic Notes in Theoretical Computer Science, pp 105-120, Elsevier, 2004. (DOI).
Polyadic History-Dependent Automata for the Fusion Calculus. Emilio Tuosto, Björn Victor, and Kidane Yemane. IT Technical Reports nr 2003-062, 2003. (External link).
Solos in Concert. Cosimo Laneve and Björn Victor. In Mathematical Structures in Computer Science, volume 13, number 5, pp 657-683, 2003. (DOI).
Solo diagrams. Cosimo Laneve, Joachim Parrow, and Björn Victor. In Proceedings of TACS 2001, pp 127-144, 2001. (External link).
Trios in Concert. Joachim Parrow. In Proof, Language and Interaction, Essays in Honor of Robin Milner, pp 621-637, MIT Press, 2000.
Concurrent Constraints in the Fusion Calculus. Björn Victor and Joachim Parrow. In Proceedings of ICALP'98, pp 455-469, 1998. (DOI).
The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes. Joachim Parrow and Björn Victor. In Proceedings of LICS'98, pp 176-185, 1998. (DOI).
Algebraic Theories of Name-Passing Calculi. Joachim Parrow and Davide Sangiorgi. In Information and Computation, volume 120, number 2, pp 174-197, 1995.
Interaction Diagrams. Joachim Parrow. In Nordic Journal of Computing, volume 2, number 4, pp 407-443, 1995.
The Mobility Workbench: A Tool for the Pi-Calculus. Björn Victor and Faron Moller. In Proceedings of CAV'94, pp 428-440, 1994. (DOI).
Modal Logics for Mobile Processes. Joachim Parrow, Robin Milner, and David Walker. In Theoretical Computer Science, volume 114, number 1, pp 149-171, 1993. (DOI).
A Calculus of Mobile Processes - Part I. Robin Milner, Joachim Parrow, and David Walker. In Information and Computation, volume 100, number 1, pp 1-40, 1992. (DOI).
A Calculus of Mobile Processes - Part II. Joachim Parrow, Robin Milner, and David Walker. In Information and Computation, volume 100, pp 41-77, 1992. (DOI).
An Algebraic Verification of a Mobile Network. Fredrik Orava and Joachim Parrow. In Formal Aspects of Computing, volume 4, number 6, pp 497-543, 1992. (DOI).