A Presheaf Semantics of Value-Passing Processes

Abstract

This paper investigates presheaf models for process calculi with
value passing. Denotational semantics in presheaf models are shown
to correspond to operational semantics in that bisimulation obtained
from open maps is proved to coincide with bisimulation as defined
traditionally from the operational semantics. Both "early" and "late"
semantics are considered, though the more interesting "late" semantics
is emphasised. A presheaf model and denotational semantics is proposed
for a language allowing process passing, though there remains
the problem of relating the notion of bisimulation obtained from open
maps to a more traditional definition from the operational semantics.
A tentative beginning is made of a "domain theory" supporting
presheaf models.