Paper: The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes (at LICS 1998)

Authors: Joachim Parrow Björn Victor

Abstract

We present the fusion calculus as a significant step towards a canonical calculus of concurrency. It simplifies and extends the π-calculus. The fusion calculus contains the polyadic π-calculus as a proper subcalculus and thus inherits all its expressive power. The gain is that fusion contains actions akin to updating a shared state, and a scoping construct for bounding their effects. Therefore it is easier to represent computational models such as concurrent constraints formalisms. It is also easy to represent the so called strong reduction strategies in the λ-calculus, involving reduction under abstraction. In the λ-calculus these tasks require elaborate encodings. Our results on the fusion calculus in this paper are the following. We give a structured operational semantics in the traditional style. The novelty lies in a new kind of action, fusion actions for emulating updates of a shared state. We prove that the calculus contains the π-calculus as a subcalculus. We define and motivate the bisimulation equivalence and prove a simple characterization of its induced congruence, which is given two versions of a complete axiomatization for finite terms. The expressive power of the calculus is demonstrated by giving a straight-forward encoding of the strong lazy λ-calculus, which admits reduction under λ abstraction

BibTeX

  @InProceedings{ParrowVictor-TheFusionCalculusEx,
    author = 	 {Joachim Parrow and Björn Victor},
    title = 	 {The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes},
    booktitle =  {Proceedings of the Thirteenth Annual IEEE Symposium on Logic in Computer Science (LICS 1998)},
    year =	 {1998},
    month =	 {June}, 
    pages =      {176--185},
    location =   {Indianapolis, IN, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }