×

Asynchronous process calculi: The first- and higher-order paradigms. (English) Zbl 0956.68081

Summary: 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

Software:

Facile; Pict
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Abramsky, S., The lazy lambda calculus, (Turner, D., Research Topics in Functional Programming (1989), Addison-Wesley: Addison-Wesley Reading, MA), 65-116
[2] Agha, G., Actorsa Model of Concurrent Computation in Distributed Systems (1986), The MIT Press: The MIT Press Cambridge, MA
[3] Amadio, R.; Castellani, I.; Sangiorgi, D., On bisimulations for the asynchronous \(π\)-calculus, Proc. CONCUR ’96. On bisimulations for the asynchronous \(π\)-calculus, Proc. CONCUR ’96, Lecture Notes in Computer Science, vol. 1119 (1996), Springer: Springer Berlin · Zbl 1514.68154
[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.; 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. On the expressiveness of internal mobility in name-passing calculi, Proc. CONCUR ’96, Lecture Notes in Computer Science, vol. 1119 (1996), Springer: Springer Berlin · Zbl 1514.68157
[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.; 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 \(π\); G. Boudol, Asynchrony and the \(π\)
[8] Boudol, G., The pi-calculus in direct style, Proc. 24th POPL (1997), ACM Press: ACM Press New York
[9] J. Despeyroux, Higher-order specification of the pi-calculus, to appear in Proc. IFIP TCS ’2000, Japan, August 2000.; 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.; 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: ACM Press New York
[13] Giacalone, A.; Mishra, P.; Prasad, S., FACILE, a symmetric integration of concurrent and functional programming, (Diaz, J.; Orejas, F., TAPSOFT ’89. TAPSOFT ’89, Lecture Notes in Computer Science, vol. 352 (1989), Springer: Springer Berlin), 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: 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 \(ν\); K. Honda, Two bisimilarities for the \(ν\)
[17] Honda, K.; Tokoro, M., An object calculus for asynchronous communications, (Tokoro, M.; Nierstrasz, O.; Wegner, P.; Yonezawa, A., ECOOP ’91 Workshop on Object Based Concurrent Programming, Geneva, Switzerland, 1991. ECOOP ’91 Workshop on Object Based Concurrent Programming, Geneva, Switzerland, 1991, Lecture Notes in Computer Science, vol. 512 (1991), Springer: Springer Berlin), 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.; 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. On asynchrony in name-passing calculi, 25th ICALP, Lecture Notes in Computer Science, vol. 1443 (1998), Springer: Springer Berlin · Zbl 0910.03019
[24] R. Milner, The polyadic \(π\); R. Milner, The polyadic \(π\)
[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, (Kuich, W., 19th ICALP. 19th ICALP, Lecture Notes in Computer Science, vol. 623 (1992), Springer: Springer Berlin), 685-695 · Zbl 1425.68298
[27] Nestmann, U.; Pierce, B., Decoding choice encodings, Proc. CONCUR ’96. Decoding choice encodings, Proc. CONCUR ’96, Lecture Notes in Computer Science, vol. 1119 (1996), Springer: Springer Berlin · Zbl 1514.68177
[28] Palamidessi, C., Comparing the expressive power of the synchronous and the asynchronous pi-calculus, Proc. 24th POPL (1997), ACM Press: 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.; 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.; 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.; 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.; 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.; 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, (Cleveland, W. R., Proc. CONCUR ’92. Proc. CONCUR ’92, Lecture Notes in Computer Science, vol. 630 (1992), Springer: Springer Berlin), 32-46
[39] B. Thomsen, Calculi for higher order communicating systems, Ph.D. Thesis, Department of Computing, Imperial College, 1990.; 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. A Facile tutorial, Proc. CONCUR ’96, Lecture Notes in Computer Science, vol. 1119 (1996), Springer: 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. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.