A game semantics of the asynchronous π-calculus

This paper studies the denotational semantics of the typed asynchronous π-calculus. We describe a simple game semantics of this language, placing it within a rich hierarchy of games models for programming languages, A key element of our account is the identification of suitable categorical structures for describing the interpretation of types and terms at an abstract level. It is based on the notion of closed Freyd category, establishing a connection between our semantics, and that of the λ-calculus. This structure is also used to define a trace operator, with which name binding is interpreted. We then show that our categorical characterization is sufficient to prove a weak soundness result. Another theme of the paper is the correspondence between justified sequences, on which our model is based, and traces in a labelled transition system in which only bound names are passed. We show that the denotations of processes are equivalent, via this correspondence, to their sets of traces. These results are used to show that the games model is fully abstract with respect to may-equivalence.