two of coins

Fusions - overview

When two names are fused, it means they can be used interchangeably. An explicit fusion is something which exists and allows the interchange. On this page I outline some threads in fusion research.

Fusion calculus. Bjorn Victor and Joachim Parrow invented the fusion calculus in 1996-1998. Their inspiration was two-fold: to simplify and make symmetric the pi calculus, and to model concurrent constraint programming.

1996Constraints as processes - encoding constraints in the pi calculus [link]
1997The update calculus - an earlier monadic form of the fusion calculus [link]
1998The fusion calculus: expressiveness and symmetry - the definitive paper introducing the fusion calculus [link]
1998The fusion calculus: expressiveness and symmetry - Victor's PhD thesis [link]
1998Concurrent constraints in the fusion calculus - gives reduction-relation and barbs [link]
1998The tau-laws of fusion - axiomatisation of replication-less calculus (NB. See also Fu's work on this). [link]

Chi calculus. Meanwhile, independently, Yuxi Fu invented the chi calculus, essentially the same as the fusion calculus. Fu was again inspired by considerations of symmetry and simplicity, and also by an analogy between reaction and cut-elimination.

1997The chi calculus - introduces the chi calculus [link]
1997A proof-theoretical approach to communication - connection with cut-elimination [link]
1999Open bisimulation on chi processes - axiomatisation, and corrects mistakes elsewhere in literature [link]
2000Chi calculus with mismatch - axiomatisation of replication-less calculus [link]

Explicit fusions. Meanwhile, independently, Gardner and Wischik came up with the explicit fusion calculus. They were inspired by an attempt to make a symmetric form of Milner's "action calculi". In retrospect (and to an expert!), explicit fusions might seem a natural way to simplify Sangiorgi's "open bisimulation".

1996A theory of bisimulation for the pi calculus - open bisimulation [link]
199?Something by Parrow about open bisimulation???
1999Symmetric action calculi - a category-theory form of explicit fusions [link]
2000Explicit fusions - first introduces explicit fusions [link]
2001Explicit fusions: theory and implementation - Wischik's PhD thesis, has more explicit fusion theory [link]
...Strong bisimulation for explicit fusions - work in progress [link]

Equators. The ability to interchange names - like an explicit fusion - can be encoded in a pi process !u(x).vx | !v(x).ux. These are called Equators. They were first mentioned by Honda and Yoshida. Merro has used equators to encode the asynchronous fusion calculus into the pi calculus.
1995On reduction-based program semantics - first mention of equators [link]
1998On the expressiveness of chi, update and fusion calculi - encoding fusions into pi calculus using equators [link]
1999On equators in asynchronous name-passing calculi without pattern-matching - bisimulation for equators [link]
2000Locality in the pi calculus and applications to distributed objects - Merro's PhD thesis [link]

Solos calculus. Fusions come about naturally in a pi-like calculus with non-binding input. Interestingly, non-binding input allows for all continuations to be encoded away without losing expressiveness. This work is mainly by Laneve, Parrow and Victor.

2000Trios in concert - partially encode continuations within the pi calculus [link]
1999Solos in concert - wholly encode continuations within fusion calculus [link]
2001Solo diagrams - how to encode replication in solos [link]
2001Explicit fusions: theory and implementation - contains a stronger encoding of continuations and proof of its efficiency [link]

Implementation. Fusions seem to arise naturally when one makes a distributed channel-based implementation of the pi calculus (Cardelli first came up with a single processor channel-based implementation). Wischik, Gardner and Laneve are working on one implementation, along with students at the University of Bologna. Meredith (author of MS Biztalk, itself based on the pi calculus) is working on another.

1985An implementation model of rendezvous communication - single-processor channel machine [link]
2001Fusion machine prototype - an online implementation of the fusion machine, a distributed abstract machine for the pi calculus [link]
2001Explicit fusions: theory and implementation - Wischik's PhD thesis contains more detail on the fusion machine [link]
2002Fusion machine - a distributed abstract machine for pi calculus [link]
...A distributed prototype of the fusion machine in jocaml - undergraduate thesis by Agostinelli, in progress
...Implementing the fusion machine in prolog - undergraduate thesis by Mazzara, in progress
...Xspresso - Microsoft distributed implementation, in progress

Linear logic. In 1993, Abramsky suggested a connection between cut elimination in linear logic, and concurrent interaction. This idea has been taken up in the chi calculus, the solos calculus, and most recently by Meredith at Microsoft.

1993Computational interpretations of linear logic - introduces linear logic, suggests concurrent connection [link]
1997A proof-theoretical approach to communication - cut-elimination and chi calculus [link]
2001Solo diagrams - interaction diagrams and petri nets in the solos calculus [link]
...Xspresso - uses full linear logic for data-types interaction. In progress.

References

Some of the papers cited above are not available online, or do not have bibtex listings online. For completeness I list them here.

The chi calculus. Not available online.

@InProceedings{fu97_chi,
  author = "Yuxi Fu",
  title  = "The Chi-Calculus",
  booktitle = "ICAPDC'97",
  year   = 1997,
  organization = "IEEE",
  pages  = "74--81",
  publisher = "Computer Society Press",
}

A proof-theoretical approach to communication. Not available online.

@InProceedings{fu97_chi_cut_elim,
  author = "Yuxi Fu",
  title  = "A proof-theoretical approach to communication",
  booktitle = "ICALP'97",
  year   = 1997,
  editor = "Pierpaolo Degano and Roberto Gorrieri and Alberto Marchetti-Spaccamela",
  volume = 1256,
  series = "Lecture Notes in Computer Science",
  pages  = "325--335",
  publisher = "Springer-Verlag",
}

Open bisimulation on chi processes. If your institution has purchased access to Springer-Verlag online, you can download PDF (237k, 16 pages).

@InProceedings{fu99_chi_axiom,
  author = "Yuxi Fu",
  title  = "Open Bisimulations on Chi Processes",
  booktitle = "CONCUR'99",
  year   = 1999,
  editor = "Jos C. M. Baeten and Sjouke Mauw",
  volume = 1664,
  series = "Lecture Notes in Computer Science",
  pages  = "304--319",
  publisher = "Springer-Verlag",
}

Chi calculus with mismatch. If you have access to Springer-Verlag online, you can download PDF (205k, 15 pages).

@InProceedings{fy2000_chi_axiom,
  author = "Yuxi Fu and Zhenrong Yang",
  title  = "Chi Calculus with Mismatch",
  booktitle = "CONCUR 2000",
  year   = 2000,
  editor = "Catuscia Palamidessi",
  volume = 1877,
  series = "Lecture Notes in Computer Science",
  pages  = "596--610",
  publisher = "Springer-Verlag",
}

A theory of bisimulation for pi-calculus. An extended abstract in CONCUR'93, LNCS715. You can [view abstract online] or [download PS.gz].

@Article{sangiorgi.open_bisimulation,
  author = "Davide Sangiorgi",
  title  = "A Theory of Bisimulation for the Pi-calculus",
  journal= "Acta Informatica",
  year   = 1996,
  volume = 33,
  pages  = "69--97",
  url    = "ftp:// ftp-sop.inria.fr/ mimosa/ personnel/ davides/ sub.ps.gz",
}

On reduction-based program semantics. [Download PS.gz].

@Article{honda_yoshida.equators,
  author = "Kohei Honda and Nobuko Yoshida",
  title  = "On Reduction-Based Process Semantics",
  journal= "Theoretical Computer Science",
  year   = 1995,
  volume = 152,
  number = 2,
  pages  = "437--486",
  url    = "ftp:// ftp.dcs.qmw.ac.uk/ lfp/ kohei/ OLD/ fst93.ps.gz",
}

Locality in the pi-calculus and applications to distributed objects. [Download PS.gz].

@PhDThesis{mer00_thesis,
  author = "Massimo Merro",
  title  = "Locality in the pi-calculus and applications to distributed objects",
  school = "{\'E}cole des Mines, France",
  year   = 2000,
  url    = "http:// www.cogs.susx.ac.uk/ users/ massimo/ phdthesis.ps.gz",
}

Trios in concert. [Download PS.gz].

@InProceedings{parrow_trios,
  author =       "Joachim Parrow",
  title =        "Trios in Concert",
  booktitle =    "Proof, Language and Interaction: Essays in Honour of {R}obin {M}ilner",
  editor =       "Gordon Plotkin and Colin Stirling and Mads Tofte",
  year =         "2000",
  pages =        "621--637",
  publisher =    "MIT Press",
  url =          "http:// www.it.kth.se/ ~joachim/ trios.ps.gz",
}

An implementation model of rendezvous communication. [Abstract] [Download PDF].

@InProceedings{car85_rendezvous,
  author = "Luca Cardelli",
  title  = "An implementation model of rendezvous communication",
  booktitle = "Seminar on Concurrency",
  year   = 1984,
  editor = "S. D. Brookes and A. W. Roscoe and G. Winskel",
  volume = 197,
  pages  = "449--457",
  series = "Lecture Notes in Computer Science",
  publisher = "Springer-Verlag",
  url    = "http:// research.microsoft.com/ Users/ luca/ Papers/ Rendezvous.A4.pdf",
}

Computational interpretations of linear logic. [Abstract]. The full version is only available online if your institution has bought access to Theoretical Computer Science.

@Article{abr93_linear_int,
  author =       "Samson Abramsky",
  title =        "Computational interpretations of linear logic",
  journal =      "Theoretical Computer Science",
  volume =       "111",
  number =       "1--2",
  pages =        "3--57",
  year =         1993,
}
Wischik | Lucian | Research | Fusions. Last updated June 2002.