Mobile Calculi based on Domains


A general name binding mechanism

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

Abstract

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.

@InProceedings\{boreale.buscemi.montanari:general-name-binding-mechanism,
  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 = \{http://mikado.di.fc.ul.pt/repository/boreale.buscemi.montanari_general-name-binding-mechanism.pdf}
}


About this site. Last modified: Fri Mar 29 15:58:29 CET 2024