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. © Springer-Verlag Berlin Heidelberg 2005.
CITATION STYLE
Boreale, M., Buscemi, M. G., & Montanari, U. (2005). A general name binding mechanism. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3705 LNCS, pp. 61–74). https://doi.org/10.1007/11580850_5
Mendeley helps you to discover research relevant for your work.