A game semantics of the asynchronous π-calculus

Research output: Chapter or section in a book/report/conference proceedingChapter in a published conference proceeding

23 Citations (SciVal)


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.

Original languageEnglish
Title of host publicationCONCUR 2005 – Concurrency Theory
Subtitle of host publicationProceedings of 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005
EditorsM. Abadi, L. Alfaro
Place of PublicationBerlin, Germany
PublisherSpringer Verlag
Number of pages15
ISBN (Print)9783540283096
Publication statusPublished - 2005
Event16th International Conference on Concurrency Theory, CONCUR 2005 - San Francisco, CA, USA United States
Duration: 23 Aug 200526 Aug 2005

Publication series

NameLecture Notes in Computer Science


Conference16th International Conference on Concurrency Theory, CONCUR 2005
Country/TerritoryUSA United States
CitySan Francisco, CA


Dive into the research topics of 'A game semantics of the asynchronous π-calculus'. Together they form a unique fingerprint.

Cite this