Presheaf models for the π-calculus

Gian Luca Cattani, Ian Stark, Glynn Winskel

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

Recent work has shown that presheaf categories provide a general model of concurrency, with an inbuilt notion of bisimulation based on open maps. Here it is shown how this approach can also handle systems where the language of actions may change dynamically as a process evolves. The example is the π-calculus, a calculus for 'mobile processes' whose communication topology varies as channels are created and discarded. A denotational semantics is described for the π-calculus within an indexed category of profunctors; the model is fully abstract for bisimilarity, in the sense that bisimulation in the model, obtained from open maps, coincides with the usual bisimulation obtained from the operational semantics of the π-calculus. While attention is concentrated on the 'late' semantics of the π-calculus, it is indicated how the 'early' and other variants can also be captured.
Original languageEnglish
Title of host publicationCategory Theory and Computer Science
Subtitle of host publication7th International Conference, CTCS '97 Santa Margherita Ligure Italy, September 4–6, 1997 Proceedings
EditorsEugenio Moggi, Giuseppe Rosolini
PublisherSpringer
Pages106-126
Number of pages21
ISBN (Electronic)978-3-540-69552-3
ISBN (Print)978-3-540-63455-3
DOIs
Publication statusPublished - 1997

Publication series

NameLecture Notes in Computer Science
PublisherSpringer Berlin / Heidelberg
Volume1290
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Fingerprint

Dive into the research topics of 'Presheaf models for the π-calculus'. Together they form a unique fingerprint.

Cite this