A General Name Binding Mechanism
- 234 Downloads
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.
KeywordsOperational Semantic Expressive Power Parallel Composition Binding Mechanism Label Transition System
Unable to display preview. Download preview PDF.
- 3.Meredith, L.G., Bjorg, S., Richter, D.: Highwire Language Specification Version 1.0. (Unpublished manuscript)Google Scholar
- 4.Microsoft Corp. Biztalk Server, http://www.microsoft.com/biztalk
- 5.Milner, R.: The Polyadic pi-Calculus: a Tutorial. Technical Report, Computer Science Dept., University of Edinburgh (1991)Google Scholar
- 8.Palamidessi, C.: Comparing the Expressive Power of the Synchronous and the Asynchronous pi-calculus. In: Conf. Rec. of POPL 1997 (1997)Google Scholar
- 10.Parrow, J., Victor, B.: The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes. In: Proc. of LICS 1998. IEEE Computer Society Press, Los Alamitos (1998)Google Scholar
- 12.Sangiorgi, D.: Expressing Mobility in Process Algebras: First-Order and Higher-Order Paradigms. PhD thesis, Department of Computer Science, University of Edinburgh (1992)Google Scholar
- 14.Victor, B.: The Fusion Calculus: Expressiveness and Symmetry in Mobile Processes. PhD thesis, Department of Computer Systems, Uppsala University (1998)Google Scholar