Concrete Process Categories

AbstractThis paper presents a rather concrete view of a semantic universe for typed concurrent computation. Starting with a notion of sets and functions organized in a category B featuring the type theory at hand, we identify the lax slice F//Span ( B ) of pseudo-functors from a free category into the bicategory of spans over B and triangles commuting up-to a lax natural transformation with representable components as a category of models of concurrency over which the semantic universe unfolds. By analogy, we call the objects of F//Span ( B ) categorical transition systems and demonstrate their relevance in giving meaning to a range of everyday phenomena including message passing among imperative programs. We identify the bicategory of spans Span(F//Span ( B )) as organizing processes at a basic level and address the question of their equality, articulated as bisimulation w.r.t. actions observable at the interfaces given by the legs of such spans. An appropriate notion of simulation yields a system of open maps by which to quotient Span(F//Span ( B )), a construction originally considered by Cockett and Spooner in its generality. The resulting process category Proc(F//Span ( B ),ϖ) properly contains the well-known interaction category SProc introduced by Abramsky et al