Asynchronous process calculi: The first- and higher-order paradigms.

*(English)*Zbl 0956.68081Summary: We compare the first- and the higher-order paradigms for the representation of mobility in process calculi. The prototypical calculus in the first-order paradigm is the \(\pi\)-calculus. Here, we focus on an asynchronous \(\pi\)-calculus \((L\pi)\) that may be regarded as the basis of some experimental programming languages (or proposal of programming languages) like Pict, Join, Blue. We extend \(L\pi\) so to allow the communication of higher-order values, that is values that may contain processes, and show that the extension does not add expressiveness: the resulting higher-order calculus can be compiled down into \(L\pi\). This paper is mostly a tutorial. It also contains original contributions. The main one is the full abstraction proof, which, with respect to previous proofs, is simpler and does not rely on certain non-finitary features of the languages such as infinite summation. Another contribution is the study of optimisations of the compilation, with which we are able to handle recursive types and to prove full abstraction also for strong behavioural equivalences.

##### MSC:

68Q55 | Semantics in the theory of computing |

PDF
BibTeX
XML
Cite

\textit{D. Sangiorgi}, Theor. Comput. Sci. 253, No. 2, 311--350 (2001; Zbl 0956.68081)

Full Text:
DOI

##### References:

[1] | Abramsky, S., The lazy lambda calculus, (), 65-116 |

[2] | Agha, G., Actorsa model of concurrent computation in distributed systems, (1986), The MIT Press Cambridge, MA |

[3] | Amadio, R.; Castellani, I.; Sangiorgi, D., On bisimulations for the asynchronous π-calculus, proc. CONCUR ’96, Lecture notes in computer science, vol. 1119, (1996), Springer Berlin |

[4] | R.M. Amadio, L. Cardelli, Subtyping recursive types, ACM Trans. Program. Languages Systems 15 (4) (1993), 575-631. A preliminary version appeared in POPL ’91 and as DEC Systems Research Center Research Report Number 62, August 1990, pp. 104-118. |

[5] | Boreale, M., On the expressiveness of internal mobility in name-passing calculi, proc. CONCUR ’96, Lecture notes in computer science, vol. 1119, (1996), Springer Berlin |

[6] | G. Boudol, Towards a lambda calculus for concurrent and communicating systems, TAPSOFT ’89, Lecture Notes in Computer Science, vol. 351, pp. 149-161, 1989. |

[7] | G. Boudol, Asynchrony and the π-calculus, Tech. Rep. RR-1702, INRIA-Sophia Antipolis, 1992. |

[8] | Boudol, G., The pi-calculus in direct style, proc. 24th POPL, (1997), ACM Press New York |

[9] | J. Despeyroux, Higher-order specification of the pi-calculus, to appear in Proc. IFIP TCS ’2000, Japan, August 2000. · Zbl 0998.68538 |

[10] | W. Ferreira, M. Hennessy, A. Jeffrey, A theory of weak bisimulation for core CML, Tr 95:05, School of Cognitive and Computing Sciences, University of Sussex, 1995. · Zbl 1345.68049 |

[11] | Fischer, M.J.; Lynch, N.A.; Paterson, M.S., Impossibility of distributed consensus with one faulty processor, J. ACM, 32, 2, 374-382, (1985) · Zbl 0629.68027 |

[12] | Fournet, C.; Gonthier, G., The reflexive chemical abstract machine and the join calculus, proc. 23rd POPL, (1996), ACM Press New York |

[13] | Giacalone, A.; Mishra, P.; Prasad, S., FACILE, a symmetric integration of concurrent and functional programming, (), 189-209 |

[14] | Gordon, A.D.; Rees, G.D., Bisimilarity for a first-order calculus of objects with subtyping, proc. 23rd POPL, (1996), ACM Press New York |

[15] | Hewitt, C., Viewing control structures as patterns of passing messages, J. artificial intelligence, 8, 3, 323-364, (1977) |

[16] | K. Honda, Two bisimilarities for the ν-calculus, Tech. Rep. 92-002, Keio University, 1992. |

[17] | Honda, K.; Tokoro, M., An object calculus for asynchronous communications, (), 133-147 |

[18] | Honda, K.; Tokoro, M., A small calculus for concurrent objects, ACM OOPS messanger, 2, 2, 50-54, (1991) |

[19] | Honda, K.; Yoshida, N., On reduction-based process semantics, Theoret. comput. sci., 152, 2, 437-486, (1995) · Zbl 0871.68122 |

[20] | Howe, D.J., Proving congruence of bisimulation in functional programming languages, Inform. comput., 124, 2, 103-112, (1996) · Zbl 0853.68073 |

[21] | H. Hüttel, J. Kleist, M. Merro, U. Nestmann, Migration=cloning; aliasing, to be presented at Sixth Workshop on Foundations of Object-Oriented Languages (FOOL 6), 1999. |

[22] | Jonsson, B.; Parrow, J., Deciding bisimulation equivalences for a class of non-finite-state programs, Inform. comput., 107, 272-302, (1993) · Zbl 0799.68133 |

[23] | Merro, M.; Sangiorgi, D., On asynchrony in name-passing calculi, 25th ICALP, Lecture notes in computer science, vol. 1443, (1998), Springer Berlin |

[24] | R. Milner, The polyadic π-calculus: a tutorial, Tech. Rep. ECS-LFCS-91-180, LFCS, Department of Computer Science Edinburgh University October 1991, Also in: F.L. Bauer, W. Brauer, H. Schwichtenberg (Eds.), Logic and Algebra of Specification, Springer, Berlin, 1993. |

[25] | Milner, R., Functions as processes, J. math. struct. comp. sci., 2, 2, 119-141, (1992) · Zbl 0773.03012 |

[26] | Milner, R.; Sangiorgi, D., Barbed bisimulation, (), 685-695 |

[27] | Nestmann, U.; Pierce, B., Decoding choice encodings, proc. CONCUR ’96, Lecture notes in computer science, vol. 1119, (1996), Springer Berlin |

[28] | Palamidessi, C., Comparing the expressive power of the synchronous and the asynchronous pi-calculus, proc. 24th POPL, (1997), ACM Press New York |

[29] | Parrow, J.; Sangiorgi, D., Algebraic theories for name-passing calculi, Inform. comput., 120, 2, 174-197, (1995) · Zbl 0836.03020 |

[30] | B.C. Pierce, D.N. Turner, Pict: a programming language based on the pi-calculus, Tech. Rep. CSCI 476, Indiana University, 1997, in: Gordon Plotkin, Colin Stirling, and Mads Tofte (Eds.) Proof, Language and Interaction: Essays in Honour of Robin Milner (Eds.) MIT Press, Cambridge, MA, to appear. |

[31] | J. Reppy. CML: a higher-order concurrent language, in: Programming Language Design and Implementation, SIGPLAN, ACM, 1991. |

[32] | D. Sangiorgi, Expressing mobility in process algebras: first-order and higher-order paradigms. Ph.D. thesis CST-99-93, Department of Computer Science, University of Edinburgh, 1992. |

[33] | D. Sangiorgi, Lazy functions and mobile processes. Tech. Rep. RR-2515, INRIA-Sophia Antipolis, 1995, in Festschrift volume in honor of Robin Milner’s 60th birthday, MIT Press, New York, to appear. |

[34] | Sangiorgi, D., Bisimulation for higher-order process calculi, Inform. comput., 131, 2, 141-178, (1996) · Zbl 0876.68042 |

[35] | Sangiorgi, D., π-calculus, internal mobility and agent-passing calculi, Theor. comput. sci., 167, 2, 235-274, (1996) · Zbl 0874.68103 |

[36] | Sangiorgi, D., The name discipline of receptiveness, Theoret. comput. sci., 221, 457-493, (1999) · Zbl 0930.68035 |

[37] | D. Sangiorgi, Interpreting functions as pi-calculus processes: a tutorial, Revised version of TR RR-3470, INRIA-Sophia Antipolis, Available from the author’s web page. |

[38] | Sangiorgi, D.; Milner, R., The problem of weak bisimulation up to, (), 32-46 |

[39] | B. Thomsen, Calculi for higher order communicating systems, Ph.D. Thesis, Department of Computing, Imperial College, 1990. |

[40] | Thomsen, B., Plain CHOCS, a second generation calculus for higher-order processes, Acta inform., 30, 1-59, (1993) · Zbl 0790.68069 |

[41] | Thomsen, B.; Leth, L.; Kuo, T.-M., A facile tutorial, proc. CONCUR ’96, Lecture notes in computer science, vol. 1119, (1996), Springer Berlin |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.