An Operational Understanding of Bisimulation from Open Maps
Glynn Winskel · Electronic Notes in Theoretical Computer Science · 1998
Models can be given to a range of programming languages combining concurrent and functional features in which presheaf categories are used as the semantic domains (instead of the more usual complete partial orders). Once this is done the languages inherit a notion of bisimulation from the “open” maps associated with the presheaf categories. However, although there are methodological and mathematical arguments for favouring semantics using presheaf categories—in particular, there is a “domain theory” based on presheaf categories which systematises bisimulation at higher-order—it is as yet far from a routine matter to read off an “operational characterisation”; by this I mean an equivalent coinductive definition of bisimulation between terms based on the operational semantics. I hope to illustrate the issues on a little process-passing language. This is joint work with Gian Luca Cattani.