×

zbMATH — the first resource for mathematics

A fully abstract denotational semantics for the calculus of higher-order communicating systems. (English) Zbl 0974.68109
In this paper we study the Calculus of Higher Order Communicating Systems (CHOCS) [B. Thomsen, Proc. of POPL’89, ACM, 1989, pp. 143-154; Inform. Comput. 116, No. 1, 38-57 (1995; Zbl 0823.68061)] in a denotational setting. We present a construction of a denotational semantics for CHOCS which resides in a domain constructed using the standard constructions of separated sum, Cartesian product, the Plotkin power domain constructor and recursively defined domains. We show, under mild restrictions, that the denotational semantics and the operational semantics of CHOCS are fully abstract. We have previously proved using bisimulation arguments that processes as first class objects are powerful enough to simulate recursion. However, the proof is very long and tedious. To demonstrate the power of the denotational approach we use it to obtain a very simple proof of the simulation of recursion result.

MSC:
68Q55 Semantics in the theory of computing
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Abramsky, S., Observation equivalence as a testing equivalence, Theoret. comput. sci., 53, 225-241, (1987) · Zbl 0626.68016
[2] Abramsky, S., Domain theory in logical form, Ann. pure appl. logic, 51, 1-77, (1991) · Zbl 0737.03006
[3] Abramsky, S., A domain equation for bisimulation, Inform. and comput., 92, 2, 161-218, (1991) · Zbl 0718.68057
[4] Abramsky, S., Proofs as processes, Theoret. comput. sci., 135, 5-9, (1994) · Zbl 0850.68297
[5] S. Abramsky, A game semantics for Idealized Algol, unpublished lecture, 1995.
[6] Abramsky, S., Interaction categories and communicating sequential processes, (), 1-15
[7] Abramsky, S., Semantics of interaction, Proc. clics summer school, Isaac Newton institute, (1996), Cambridge University Press Cambridge
[8] S. Abramsky, R. Jagadeesan, P. Malacaria, Full abstraction for PCF, Inform. Comput. (2000) to appear. · Zbl 1006.68028
[9] Barendregt, H.P., The lambda calculus — its syntax and semantics, (1984), North-Holland Amsterdam · Zbl 0551.03007
[10] Boudol, G., (), 149-161
[11] P. Christensen, The domain of CSP processes, incomplete draft, The Technical University of Denmark, 1988.
[12] Hennessy, M., A term model for synchronous processes, Inform. and control, 51, 1, 58-75, (1981) · Zbl 0503.68022
[13] M. Hennessy, A fully abstract denotational model for higher-order processes (extended abstract), Proc., 8th Annu. IEEE Symp. on Logic in Computer Science, Montreal, Canada, 19-23, June 1993, pp. 397-408.
[14] Hennessy, M., A fully abstract denotational model for higher-order processes, Inform. and comput., 112, 1, 55-95, (1994) · Zbl 0806.68071
[15] Hennessy, M., (), 286-303
[16] Hennessy, M.; Milner, R., Algebraic laws for nondeterminism and concurrency, J. assoc. comput. Mach., 32, 1, 137-161, (1985) · Zbl 0629.68021
[17] Hennessy, M.; Plotkin, G., (), 261-274
[18] M. Hyland, C.H.L. Ong, On full abstraction for PCF, Inform. and Comput. (2000) to appear. · Zbl 1006.68027
[19] A. Ingólfsdóttir, B. Thomsen, Semantic models for CCS with values, Proc. Chalmers Workshop on Concurrency, May 1991.
[20] R. Jagadeesan, P. Panangaden, A domain-theoretic model for a higher-order process calculus, Proc. ICALP 90, Lecture Notes in Computer Science, vol. 443, Springer, Berlin, 1990, pp. 181-194. · Zbl 0766.68089
[21] Kennaway, J.R.; Sleep, M.R., A denotational semantics for first class processes, Draft, school of information systems, (1988), University of East Anglia Norwich
[22] Milne, G.; Milner, R., Concurrent processes and their syntax, J. assoc. comput. Mach., 26, 2, 302-321, (1979) · Zbl 0395.68030
[23] Milner, R., (), 157-173
[24] Milner, R., A calculus of communicating systems, Lecture notes in computer science, vol. 92, (1980), Springer Berlin · Zbl 0452.68027
[25] Milner, R., (), 25-34
[26] Milner, R., Calculi for synchrony and asynchrony, Theoret. comput. sci., 25, 267-310, (1983) · Zbl 0512.68026
[27] Milner, R., Communication and concurrency, (1989), Prentice-Hall Englewood cliffs, NJ · Zbl 0683.68008
[28] Milner, R.; Parrow, J.; Walker, D., A calculus of mobile processes, parts I and II, Inform. and comput., 100, 1-77, (1992)
[29] Park, D., Concurrency and automata on infinite sequences, Theoretical computer science VII, lecture notes in computer science, vol. 104, (1981), Springer Berlin · Zbl 0457.68049
[30] Pitts, A.M.; Stark, I.D.B., (), 122-141
[31] Plotkin, G., A powerdomain construction, SIAM J. comput., 5, 452-487, (1976) · Zbl 0355.68015
[32] G. Plotkin, A structural approach to operational semantics, Technical Rep. DAIMI FN-19, Computer Science Department, Aarhus University, 1981.
[33] G. Plotkin, Post-graduate notes in advanced domain theory (incorporating the “Pisa Notes”), Department of Computer Science, University of Edinburgh, 1981.
[34] Plotkin, G., (), 360-372
[35] Sangiorgi, D., (), 151-166
[36] Smyth, M.B., Powerdomains, J. comput. systems sci., 16, 1, 23-36, (1978) · Zbl 0408.68017
[37] Stark, I., Categorical models for local names, Lisp symbolic comput., 9, 1, 77-107, (1996)
[38] Stark, I., (), 36-42
[39] Stirling, C., Modal logics for communicating systems, Theoret. comput. sci., 49, 311-347, (1987) · Zbl 0624.68019
[40] A. Tarski, A lattice-theoretical fixpoint theorem and its applications, Pacific J. Math. 5 (1955) 285-309. · Zbl 0064.26004
[41] B. Thomsen, A calculus of higher-order communicating systems, Proc. POPL 89, The Association for Computing Machinery, New York, 1989, pp. 143-154.
[42] B. Thomsen, Calculi for higher-order communicating systems, Ph.D. Thesis, Imperial College, London University, 1990.
[43] Thomsen, B., Plain CHOCS. A second generation higher-order calculus for higher-order processes, Acta inform., 30, 1, 1-59, (1993) · Zbl 0790.68069
[44] Thomsen, B., A theory of higher-order communicating systems, Inform. and comput., 116, 1, 38-57, (1995) · Zbl 0823.68061
[45] Walker, D., (), 186-192
[46] Winskel, G., (), 392-410
[47] Winskel, G., A linear metalanguage for concurrency, Proc. AMAST’98, Brazil, lecture notes in computer science, vol. 1548, (1999), Springer Berlin · Zbl 0921.18007
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.