A Categorical Model of an i/o-typed pi-calculus
This paper introduces a new categorical structure that is a model of a variant of the i/o-typed pi-calculus, in the same way that a cartesian closed category is a model of the \lambda-calculus. To the best of our knowledge, no categorical model has been given for the i/o-typed pi-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 relevance of the categorical model, we show by a semantics consideration that the pi-calculus is equivalent to a core calculus of concurrent ML.
Wed 10 AprDisplayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change
14:00 - 16:00 | |||
14:00 30mTalk | Asynchronous timed session types: duality and time-sensitive processes ESOP Laura Bocchi University of Kent, Maurizio Murgia , Vasco T. Vasconcelos University of Lisbon, Portugal, Nobuko Yoshida Imperial College London Link to publication | ||
14:30 30mTalk | Manifest Deadlock-Freedom for Shared Session Types ESOP Stephanie Balzer Carnegie Mellon University, Bernardo Toninho Imperial College London, Frank Pfenning Carnegie Mellon University, USA Link to publication | ||
15:00 30mTalk | A Categorical Model of an i/o-typed pi-calculus ESOP Link to publication | ||
15:30 30mTalk | A Process Algebra for Link Layer Protocols ESOP Link to publication |