A THEORY OF HIGHER-ORDER COMMUNICATING SYSTEMS

A calculus of higher order communicating systems (CHOCS) was presented by the author in [''Proceedings of POPL 89,'' pp. 143-154, Assoc. Com puting Machinery, New York]. This calculus considers sending and recei ving processes to be as fundamental as nondeterminism and parallel com position. In this paper we present an investigation of the foundation of the theory of this calculus, together with the full proofs of all m ajor theorems. CHOCS is an extension of Milner's Calculus of Communica ting Systems (CCS) in the sense that all the constructions of CCS are included or may be derived from more fundamental constructs. Most of t he mathematical framework of CCS carries over almost unchanged. The op erational semantics of CHOCS is given as a labelled transition system and it is a direct extension of the semantics of CCS with value passin g. A set of algebraic laws satisfied by the calculus is presented. The se are similar to the CCS laws, varying only by introducing obvious ex tra laws for sending and receiving processes. The power of process pas sing is underlined by a result showing that recursion can be simulated by means of process passing and communication. (C) 1995 Academic Pres s, Inc.