Mobile Calculi based on Domains

A general name binding mechanism

M. Boreale and M.G. Buscemi and U. Montanari


We study fusion and binding mechanisms in name passing process calculi. To this purpose, we introduce the U-Calculus, a process calculus with no I/O polarities and a unique form of binding. The latter can be used both to control the scope of fusions and to handle new name generation. This is achieved by means of a simple form of typing: each bound name x is annotated with a set of exceptions, that is names that cannot be fused to x. The new calculus is proven to be more expressive than pi-calculus and Fusion calculus separately. In U-Calculus, the syntactic nesting of name binders has a semantic meaning, which cannot be overcome by the ordering of name extrusions at runtime. Thanks to this mixture of static and dynamic ordering of names, U-Calculus admits a form of labelled bisimulation which is a congruence. This property yields a substantial improvement with respect to previous proposals by the same authors aimed at unifying the above two languages. The additional expressiveness of U-Calculus is also explored by providing a uniform encoding of mixed guarded choice into the choice-free sub-calculus.

  author = \{M. Boreale and M.G. Buscemi and U. Montanari},
  title = \{A general name binding mechanism},
  booktitle = \{Proceedings of Trustworthy Global Computing 2005 (TGC05)},
  year = \{2005}, 
  series = \{LNCS}, 
  publisher = \{Springer}, 
  url = \{}

About this site. Last modified: Fri Sep 22 08:15:47 CEST 2017