A denotational semantics is given for a language for distributed programming based on communication (CSP). The semantics uses both linear sequences of communications to record computations and special states, called “expectation sets,” characterizing potential deadlocks. For any well-formed program segment, the semantics is a relation between attainable states and the communication sequences needed to attain these states. In binding two or more processes we match and merge the communication sequences assumed by each process to obtain a sequence and state of the combined process. The approach taken here is distinguished by relatively simple semantic domains and ordering.

--Authors’ Abstract

The authors give a denotational semantics for CSP-like programs. The approach can be applied also for Milner’s communicating processes or other models with explicit process communication (i.e., process communication not done via shared variables). The authors claim that the approach is more general than any other presented so far, as it also applies to nested parallelism. This is a rather technical, but clearly written, paper.