A Categorical Model of an i/o-typed π-calculus

Abstract

This paper introduces a new categorical structure that is a model of a variant of the i/o-typed π-calculus, in the same way that a cartesian closed category is a model of the ⋋-calculus. To the best of our knowledge, no categorical model has been given for the i/o-typed π-calculus, in contrast to session-typed calculi, to which corresponding logic and categorical structure were given. The categorical structure introduced in this paper has a simple definition, combining two well-known structures, namely, closed Freyd category and compact closed category. The former is a model of effectful computation in a general setting, and the latter describes connections via channels, which cause the effect we focus on in this paper. To demonstrate the relevance of the categorical model, we show by a semantic consideration that the π -calculus is equivalent to a core calculus of Concurrent ML.