The earliest application of sheaf theory to concurrency I am aware of is the LICS'86 paper of Monteiro and Pereira: @InProceedings( MP, Author="Monteiro, L.F. and Pereira, F.C.N.", Title="Outline of a Sheaf-theoretic Approach to Concurrency", Booktitle="Proc. IEEE Symp. on Logic in Computer Science", Address="Boston", Month=Jul, Year=1986) My IJPP paper in the same year, @Article( Pr86, Author="Pratt, V.R.", Title="Modeling Concurrency with Partial Orders", Journal="Int. J. of Parallel Programming", Volume=15, Number=1, Pages="33-71", Month=Feb, Year=1986) (retrievable from boole.stanford.edu by anonymous ftp as /pub/ijpp.tex, see also the README in the same directory.) discusses the relationship of my semantics of networks (section 4 of my paper) with Monteiro and Pereira's semantics. Ignore the February 1986 date on that issue of IJPP, I did not send the manuscript to IJPP until after LICS'86. This permitted me to read Monteiro and Pereira's paper and address the question of what differences if any there were between my treatment and their sheaf-theoretic one. I covered this in two paragraphs (appended here) giving respectively the similarities and the differences, the latter in terms of changes sufficient to bring my treatment into juxtaposition with theirs. It may well be however that these differences are artifacts of too narrow a notion of sheaf. If the definition in my paper can be viewed as sheaf-theoretic without making those changes I would appreciate hearing the details from anyone with the requisite sheaf theory and a willingess to sort out the definitions in the respective papers. I have not worked enough with sheaves myself to trust my judgement on this. Vaughan Pratt ==========2 paragraphs on sheaves from "Modelling Concurrency with PO's"=== This approach has some important points in common with our approach, as well as some important differences. The points of correspondence are as follows. In place of a category of open sets of a topological space $X$ and their inclusions we use the category {\bf Set} whose objects (sets) provide our alphabets and whose morphisms (functions) our translations. By using arbitrary functions rather than inclusions we provide for action renaming (via non-inclusions) and ``short-circuiting'' (via non-injections). The concept of restriction has the same significance for both approaches, and is a contravariant functor in both cases. The explicit concept of section agreement on intersections, which is the essence of a sheaf, appears only implicitly in our approach, by virtue of the possibility of overlap between the $t_i(\Sigma_i)$'s. We do not require the $t_i(\Sigma_i)$'s to cover $\Sigma$, but then neither do we require that the system behavior consistent with a family of component behaviors be unique. In place of monoids we use processes made up of pomsets, which come with a built-in solution to the problem of non-injective translations and which also have the several advantages cited for them in the introduction, not achievable with monoids. Our approach may be massaged into closer correspondence with the sheaf approach by replacing the $\Sigma_i$'s with their images $t_i(\Sigma_i)$ as subsets of $\Sigma$, and the $t_i$'s with the corresponding inclusions from $t_i(\Sigma_i)$ into $\Sigma$, provided the $t_i$'s are injective and the $t_i(\Sigma_i)$'s cover $\Sigma$ (easily arranged by adding a dummy process to complete the cover). There is no loss of generality in requiring these subsets to be open since in the absence of other requirements $\Sigma$ can be equipped with the discrete topology (all subsets open). The information in the $P_i$'s is now not accessible since the $t_i$'s are gone, so, taking our sheaves to be sheaves of processes rather than of monoids, we move the $P_i$'s into the restriction functor by having $\rho$ map $t_i(\Sigma_i)$ to $t_i?+(P_i)$ where $t_i?+$ is the extension of $t_i$ to a pomset homomorphism. The remaining step is to have $\rho$ map the other subsets of $\Sigma$, or at least the arbitrary unions and finite intersections of the $t_i(\Sigma_i)$'s, to appropriate subsets of $\Sigma\ddagger$, in order to make $\rho$ into a sheaf, though we have not yet worked out the appropriate assignment.