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
Available as PostScript,
PDF,
DVI.
|