@string{brics =	"{BRICS}"}
@string{daimi =	"Department of Computer Science, University of Aarhus"}
@string{iesd  =	"Department of Computer Science, Institute
		  of Electronic Systems, Aalborg University"}
@string{rs    =	"Research Series"}
@string{ns    =	"Notes Series"}
@string{ls    =	"Lecture Series"}
@string{ds    =	"Dissertation Series"}

@TechReport{BRICS-DS-99-1,
  author = 	 "Cattani, Gian Luca",
  title = 	 "Presheaf Models for Concurrency (Unrevised)",
  institution =  brics,
  year = 	 1999,
  type = 	 ds,
  number = 	 "DS-99-1",
  address = 	 daimi,
  month = 	 apr,
  note =	 "PhD thesis. xiv+255~pp",
  abstract =	 "In this dissertation we investigate presheaf models for
concurrent computation. Our aim is to provide a systematic treatment
of bisimulation for a wide range of concurrent process
calculi. Bisimilarity is defined abstractly in terms of open maps as
in the work of Joyal, Nielsen and Winskel. Their work inspired this
thesis by suggesting that presheaf categories could provide abstract
models for concurrency with a built-in notion of bisimulation.\bibpar

We show how presheaf categories, in which traditional models of
concurrency are embedded, can be used to deduce congruence properties
of bisimulation for the traditional models. A key result is given
here; it is shown that the homomorphisms between presheaf categories,
i.e., colimit preserving functors, preserve open map bisimulation. We
follow up by observing that presheaf categories and colimit preserving
functors organise in what can be considered as a category of
non-deterministic domains. Presheaf models can be obtained as
solutions to recursive domain equations. We investigate properties of
models given for a range of concurrent process calculi, including {\bf
CCS}, {\bf CCS} with value-passing, $\pi$-calculus and a form of {\bf
CCS} with linear process passing. Open map bisimilarity is shown to be
a congruence for each calculus. These are consequences of general
mathematical results like the preservation of open map bisimulation by
colimit preserving functors. In all but the case of the higher order
calculus, open map bisimulation is proved to coincide with traditional
notions of bisimulation for the process terms. In the case of higher
order processes, we obtain a ner equivalence than the one one would
normally expect, but this helps reveal interesting aspects of the
relationship between the presheaf and the operational semantics. For a
fragment of the language, corresponding to a form of
$\lambda$-calculus, open map bisimulation coincides with applicative
bisimulation.\bibpar

In developing a suitable general theory of domains, we extend results
and notions, such as the limit-colimit coincidence theorem of Smyth
and Plotkin, from the order-enriched case to a ``fully'' 2-categorical
situation. Moreover we provide a domain theoretical analysis of (open
map) bisimulation in presheaf categories. We present, in fact,
induction and coinduction principles for recursive domains as in the
works of Pitts and of Hermida and Jacobs and use them to derive a
coinduction property based on bisimulation",
  linkhtmlabs =	 "",
  linkps =	 "",
  linkpdf =	 ""
}