Graph rewriting has been used extensively to model the behaviour of concurrent systems and to provide a formal semantics for them. In this paper, we investigate processes for Local Action Systems (LAS); LAS generalize several types of graph rewriting based on node replacement and embedding. An important difference between processes for Local Action Systems and the process notions that have been introduced for other systems, for example, Petri nets, is the presence of a component describing the embedding mechanism. The aim of the paper is to develop a methodology for dealing with this embedding mechanism: we introduce a suitable representation (a dynamic structure) for it, and then investigate the algebraic properties of this representation. This leads to a simple characterization of the configurations of a process and to a number of equational laws for dynamic structures. We illustrate the use of these laws by providing an equational proof of one of the basic results for LAS processes, namely that the construction yielding the result graph of a process behaves well with respect to the sequential composition of processes.

We define a construction operation on hypergraphs based on a colimit and show that its expressiveness is equal to the graph expressions of Bauderon and Courcelle. We also demonstrate that by closing a set of rewrite rules under graph construction we obtain a notion of rewriting equivalent to the double-pushout approach of Ehrig. The usefulness of our approach for the compositional modelling of concurrent systems is then demonstrated by giving a semantics of process graphs (corresponding to a process calculus with mobility) and of Petri nets. We introduce on the basis if a hypergraph construction, a method for the static analysis of process graphs, related to type systems.

We present an axiomatic framework for Girard's Geometry of Interaction based on the notion of linear combinatory algebra. We give a general construction on traced monoidal categories, with certain additional structure, that is sufficient to capture the exponentials of Linear Logic, which produces such algebras (and hence also ordinary combinatory algebras). We illustrate the construction on six standard examples, representing both the ‘particle-style’ as well as the ‘wave-style’ Geometry of Interaction.

We survey the main results on computability and totality in Scott–Eršov-domains as well as their applications to the theory of functionals of higher types and the semantics of functional programming languages. A new density theorem is proved and applied to show the equivalence of the hereditarily computable total continuous functionals with the hereditarily effective operations over a large class of base types.

We construct a double category [Dscr ] of proof-nets in multiplicative linear logic (MLL). Its horizontal arrows are MLL modules (subnets of well-formed nets), its vertical arrows model side-effects, and its double cells interpret the cut-elimination procedure. The categorical model is modular in the sense that every computation of a composite module (π1; π2) factors out as the separate and interacting computations of the two subcomponents π1 and π2. This enables us to trace MLL modules in the course of cut-elimination, and analyze their behaviour in time.

We show a method for translating concurrent systems into partially ordered sets in a functorial way. This is done in a way resembling the construction of the fundamental groups in topology. Since the morphisms of concurrent systems have a flavour of the implementability of one system in another, the functor provides a tool for proving certain non-implementability results.

Let Σ be an arbitrary signature and ϒ be a non-empty set of operation symbols within it. A (partial) Σ-algebra is ϒ-total when all its operations in ϒ are total: these are the partly total algebras in the title, and they include total algebras and attributed graphs. In this paper we establish a necessary and sufficient condition on a pair of homomorphisms of ϒ-total Σ-algebras for the existence of a pushout complement of them. This solves the application problem for the double-pushout transformation of these kinds of structure.

We show that Friedman's proof of the existence of non-trivial βη-complete models of λ→ can be extended to system F. We isolate a set of conditions that are sufficient to ensure βη-completeness for a model of F (and α-completeness at the level of types), and we discuss which class of models we get. In particular, the model introduced in Barbanera and Berardi (1997), having as polymorphic maps exactly all possible Scott continuous maps, is βη-complete, and is hence the first known complete non-syntactic model of F. In order to have a suitable framework in which to express the conditions and develop the proof, we also introduce the very natural notion of ‘polymax models’ of System F.

Realizability and related functional interpretations provide models for constructive mathematics. Generally, these models do not validate the axiom of choice for propositions taken over hierarchies of extensional functionals. We describe simple classes of models where the axiom is validated.

Frequently, mathematical structures of a certain type and their morphisms fail to form a category for lack of composability of the morphisms; one example of this problem is the class of probabilistic automata when equipped with morphisms that allow restriction as well as relabelling. The proper mathematical framework for this situation is provided by a generalisation of category theory in the shape of the so-called precategories, which are introduced and studied in this paper. In particular, notions of adjointness, weak adjointness and partial adjointness for precategories are presented and justified in detail. This makes it possible to use universal properties as characterisations of well-known basic constructions in the theory of (generative) probabilistic automata: we show that accessible automata and decision trees, respectively, form coreflective subprecategories of the precategory of probabilistic automata. Moreover, the aggregation of two automata is identified as a partial product, whereas restriction and interconnection of automata are recognised as Cartesian lifts.

Relational structures offer a common framework for handling graphs and hypergraphs of various kinds. Operations like disjoint union, the creation of new relations by means of quantifier-free formulas, and relabellings of relations make it possible to denote them using algebraic expressions. It is known that every monadic second-order property of a structure is verifiable in time proportional to the size of such an algebraic expression defining it. We prove here that this result remains true if we also use in these algebraic expressions a fusion operation that fuses all elements of the domain satisfying some unary predicate. The value mapping from these algebraic expressions to the structures they denote is a monadic second-order definable transduction, which means that the structure is definable inside the tree representing the algebraic expression by monadic second-order formulas. It follows (by using results of other articles) that, with this fusion operation, we cannot generate more graph families, but we can generate them with less unary auxiliary predicates. We also obtain clear-cut characterizations of Vertex Replacement and Hyperedge Replacement context-free graph grammars in terms of four types of operations, amongst which is the fusion of vertices satisfying a specified predicate.

This work is a step toward the development of a logic for types and computation that includes not only the usual spaces of mathematics and constructions, but also spaces from logic and domain theory. Using realizability, we investigate a configuration of three toposes that we regard as describing a notion of relative computability. Attention is focussed on a certain local map of toposes, which we first study axiomatically, and then by deriving a modal calculus as its internal logic. The resulting framework is intended as a setting for the logical and categorical study of relative computability.

This paper introduces a temporal logic for coalgebras. Nexttime and lasttime operators are defined for a coalgebra, acting on predicates on the state space. They give rise to what is called a Galois algebra. Galois algebras form models of temporal logics like Linear Temporal Logic (LTL) and Computation Tree Logic (CTL). The mapping from coalgebras to Galois algebras turns out to be functorial, yielding indexed categorical structures. This construction gives many examples, for coalgebras of polynomial functors on sets. More generally, it will be shown how ‘fuzzy’ predicates on metric spaces, and predicates on presheaves, yield indexed Galois algebras, in basically the same coalgebraic manner.

In standard realizability one works with respect to an untyped universe of realizers called a partial combinatory algebra (pca). It is well known that a pca [Ascr ] gives rise to a categorical model of impredicative type theory via the category Asm([Ascr ]) of assemblies over [Ascr ] or the realizability topos over [Ascr ].

Recently, John Longley introduced a typed version of pca's (Longley 1999b). The above mentioned construction of categorical models extends to the typed case. However, in general these are no longer impredicative. We show that for a typed pca [Tscr ] the ensuing models are impredicative if and only if [Tscr ] has a universal type U. Such a type U can be endowed with the structure of an untyped pca such that U and [Tscr ] induce equivalent realizability models: in other words, a typed pca [Tscr ] with a universal type is essentially untyped. Thus, a posteriori it turns out that nothing is lost by restricting to (untyped) pca's as far as realizability models of impredicative type theories are concerned.

For instance, we show that for a typed pca [Tscr ] the fibred category of discrete families in Asm([Tscr ]) is small if and only if [Tscr ] has a universal type. As the category of ¬¬-separated objects of the modified realizability topos is equivalent to Asm([Tscr ]) for an appropriate typed pca [Tscr ] without a universal type, it follows that the discrete families in the subcategory of ¬¬-separated objects of the modified realizability topos do not provide a model of polymorphic λ-calculus.

This paper describes a family of logics whose categorical semantics is based on functors with structure rather than on categories with structure. This allows the consideration of logics that contain possibly distinct logical subsystems whose interactions are mediated by functorial mappings. For example, within one unified framework, we shall be able to handle logics as diverse as modal logic, ordinary linear logic, and the ‘noncommutative logic’ of Abrusci and Ruet, a variant of linear logic that has both commutative and noncommutative connectives.

Although this paper will not consider in depth the categorical basis of this approach to logic, preferring instead to emphasise the syntactic novelties that it generates in the logic, we shall focus on the particular case when the logics are based on a linear functor, in order to give a definite presentation of these ideas. However, it will be clear that this approach to logic has considerable generality.