Abstract and behaviour module specifications

The theory of algebraic module specifications and modular systems was developed initially mainly on the basis of equational algebraic specifications. We show that it is in fact almost independent of what kind of underlying specification framework is chosen. More specifically, we present a formulation where this framework appears as an indexed category or, equivalently, specification frame. The ensuing theory is called the theory of abstract module specifications. We are able to prove main results concerning the correctness and compositionality of abstract module specifications in a purely categorical way, assuming the existence of pushouts of morphisms between abstract specifications that allow model amalgamation, functor extension and/or suitable free constructions. Then, by instantiating the theory of abstract module specifications to the behaviour specification frame in the sense of Nivela and Orejas, we obtain a theory of behaviour module specifications.

Presheaf Models for the pi-Calculus

<p>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 pi-calculus, a calculus for `mobile processes' whose communication topology varies as channels are created and discarded. A denotational semantics is described for the pi-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 pi-calculus. While attention is concentrated on the `late' semantics of the pi-calculus, it is indicated how the `early' and other variants can also be captured.</p><p> </p><p>A version of this paper appears in Category Theory and Computer Science: Proceedings of the 7th International Conference CTCS '97, Lecture Notes in Computer Science 1290. Springer-Verlag, September 1997.</p>

Locally cartesian closed categories and type theory

It is well known that for much of the mathematics of topos theory, it is in fact sufficient to use a category C whose slice categories C/A are cartesian closed. In such a category, the notion of a ‘generalized set’, for example an ‘A-indexed set’, is represented by a morphism B → A of C, i.e. by an object of C/A. The point about such a category C is that C is a C-indexed category, and more, is a hyper-doctrine, so that it has a full first order logic associated with it. This logic has some peculiar aspects. For instance, the types are the objects of C and the terms are the morphisms of C. For a given type A, the predicates with a free variable of type A are morphisms into A, and ‘proofs’ are morphisms over A. We see here a certain ‘ambiguity’ between the notions of type, predicate, and term, of object and proof: a term of type A is a morphism into A, which is a predicate over A; a morphism 1 → A can be viewed either as an object of type A or as a proof of the proposition A.