Presheaf Models for the tex2html_wrap_inline20-Calculus

Gian Luca Cattani
Ian Stark
Glynn Winskel

December 1997


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 tex2html_wrap_inline20-calculus, a calculus for `mobile processes' whose communication topology varies as channels are created and discarded. A denotational semantics is described for the tex2html_wrap_inline20-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 tex2html_wrap_inline20-calculus. While attention is concentrated on the `late' semantics of the tex2html_wrap_inline20-calculus, it is indicated how the `early' and other variants can also be captured

Available as PostScript, PDF, DVI.


Last modified: 2003-06-08 by webmaster.