Symmetries and Dualities in Name-Passing Process Calculi
- 635 Downloads
We study symmetries and duality between input and output in the \(\pi \)-calculus. We show that in dualisable versions of \(\pi \), including \(\pi \) and fusions, duality breaks with the addition of ordinary input/output types. We illustrate two proposals of calculi that overcome these problems. One approach is based on a modification of fusion calculi in which the name equivalences produced by fusions are replaced by name preorders, and with a distinction between positive and negative occurrences of names. The resulting calculus allows us to import subtype systems, and related results, from the pi-calculus. The second approach consists in taking the minimal symmetrical conservative extension of \(\pi \) with input/output types.
KeywordsType System Operational Semantic Parallel Composition Typing Rule Mobile Process
Unable to display preview. Download preview PDF.
- 2.Fu, Y.: The \(\chi \)-calculus. In: Proc. APDC, pp. 74–81. IEEE Computer Society Press (1997)Google Scholar
- 5.Hirschkoff, D., Madiot, J.M., Sangiorgi, D.: Name-Passing Calculi: From Fusions to Preorders and Types. long version of the paper presented at LICS’13, in preparation (2014)Google Scholar
- 6.Hirschkoff, D., Madiot, J.M., Xu, X.: A behavioural theory for a \(\pi \)-calculus with preorders. submitted (2014)Google Scholar
- 10.Parrow, J., Victor, B.: The fusion calculus: expressiveness and symmetry in mobile processes. In: Proc. of LICS, pp. 176–185. IEEE (1998)Google Scholar
- 13.Sangiorgi, D.: \(\pi \)-calculus, internal mobility, and agent-passing calculi. In: Selected papers from TAPSOFT ’95, pp. 235–274. Elsevier (1996)Google Scholar
- 14.Sangiorgi, D.: Lazy functions and mobile processes. In: Proof, Language, and Interaction, pp. 691–720. The MIT Press (2000)Google Scholar
- 15.Sangiorgi, D., Walker, D.: The Pi-Calculus: a theory of mobile processes. Cambridge University Press (2001)Google Scholar
- 16.van Bakel, S., Vigliotti, M.G.: An Implicative Logic based encoding of the \(\lambda \)-calculus into the \(\pi \)-calculus (2014). http://www.doc.ic.ac.uk/~svb/