A fully abstract denotational semantics for the calculus of higher-order communicating systems (Q5940933)

In this paper we study the Calculus of Higher Order Communicating Systems (CHOCS) [\textit{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.