A categorical framework for typing CCS-style process communication

Category theory has proved a useful tool in the study of type systems for sequential programming languages. Various approaches have been proposed to use categorical models to examine the type structures appropriate to concurrent systems. In this paper, we outline some of these approaches, such as interaction categories, and argue that they are not appropriate to model the handshake communication mechanism as used e.g. in CCS or the -calculus. We propose an alternative general categorical framework for examining the type structure of such systems, and exhibit its categorical structure, which is similar to that of existing approaches. We then examine in detail an instance of this framework, based on a simple fragment of CCS. We prove that it is isomorphic to a syntactic category constructed from a process algebra similar to CCS, with a fusion operator, as in the fusion calculus. Thus, we make explicit some of the type structure implicitly present in such a process algebra.

• Type: Journal
• Year: 2002
• Where: ENTCS
• Authors: Ralf Schweimeier
• Keywords: ENTCS 2002, General Categorical Framework, Sequential Programming Languages, Type Structure