A proof system for communicating processes with value-passing (Q1179808)

The language studied is essentially the original value-passing version of CCS except that \(\tau\) is replaced by versions of the internal and external choice operators from TCSP. The reasonings about data and about processes are dissociated. The main proof system is used for the reasoning about processes. For the reasoning about data a subsidiary proof system would be used or called by the main one. In the denotational model the input expression c?x.p is represented as a function mapping data-values to semantic objects. The main system is shown to be sound and complete for finite processes with respect to a denotational semantics based on Acceptance Trees.