The most popular method for establishing bisimilarities among processes is to exhibit bisimulation relations. By definition, [Rscr ] is a bisimulation relation if [Rscr ] progresses to [Rscr ] itself, i.e., pairs of processes in [Rscr ] can match each other's actions and their derivatives are again in [Rscr ].

We study generalisations of the method aimed at reducing the size of the relations to be exhibited and hence relieving the proof work needed to establish bisimilarity results. We allow a relation [Rscr ] to progress to a different relation [Fscr ] ([Rscr ]), where [Fscr ] is a function on relations. Functions that can be safely used in this way (i.e., such that if [Rscr ] progresses to [Fscr ] ([Rscr ]), then [Rscr ] only includes pairs of bisimilar processes) are sound. We give a simple condition that ensures soundness. We show that the class of sound functions contains non-trivial functions and we study the closure properties of the class with respect to various important function constructors, like composition, union and iteration. These properties allow us to construct sophisticated sound functions – and hence sophisticated proof techniques for bisimilarity – from simpler ones.

The usefulness of our proof techniques is supported by various non-trivial examples drawn from the process algebras CCS and π-calculus. They include the proof of the unique solution of equations and the proof of a few properties of the replication operator. Among these, there is a novel result that justifies the adoption of a simple form of prefix-guarded replication as the only form of replication in the π-calculus.

This paper provides an algorithm that, given two finite algebras A and B each of arbitrary finite similarity type, determines whether or not A and B are categorically equivalent. Although the algorithm is not practical in general, we consider some conditions on the algebras that improve its performance.

The context of this article is the programme to develop monoidal bicategories with a feedback operation as an algebra of processes, with applications to concurrency theory. The objective here is to study reachability, minimization and minimal realization in these bicategories. In this setting the automata are 1-cells, in contrast with previous studies where they appeared as objects. As a consequence, we are able to study the relation of minimization and minimal realization to serial composition of automata using (co)lax (co)monads. We are led to define suitable behaviour categories and prove minimal realization theorems that extend classical results.

Fokkink and Zantema (Fokkink and Zantema 1994) have shown that bisimulation equivalence has a finite equational axiomatization over the language of Basic Process Algebra with the binary Kleene star operation (BPA*). In light of this positive result on the mathematical tractability of bisimulation equivalence over BPA*, a natural question to ask is whether any other (pre)congruence relation in van Glabbeek's linear time/branching time spectrum is finitely (in)equationally axiomatizable over it. In this paper, we prove that, unlike bisimulation equivalence, none of the preorders and equivalences in van Glabbeek's linear time/branching time spectrum, whose discriminating power lies in between that of ready simulation and that of completed traces, has a finite equational axiomatization. This we achieve by exhibiting a family of (in)equivalences that holds in ready simulation semantics (which is the finest semantics that we consider) and whose instances cannot all be proved by means of any finite set of (in)equations that is sound in completed trace semantics (which is the coarsest semantics that is appropriate for the language BPA*). To this end, for every finite collection of (in)equations that are sound in completed trace semantics, we build a model in which some of the (in)equivalences of the family under consideration fail. The construction of the model mimics the one used by Conway (Conway 1971, p. 105) in his proof of a result, originally due to Redko, to the effect that infinitely many equations are needed to axiomatize equality of regular expressions.

Our non-finite axiomatizability results apply to the language BPA* over an arbitrary non-empty set of actions. In particular, we show that completed trace equivalence is not finitely based over BPA* even when the set of actions is a singleton. Our proof of this result may be adapted to the standard language of regular expressions to yield a solution to an open problem posed by Salomaa (Salomaa 1969, p. 143).

Another semantics that is usually considered in process theory is trace semantics. Trace semantics is, in general, not preserved by sequential composition, and is therefore inappropriate for the language BPA*. We show that, if the set of actions is a singleton, trace equivalence and preorder are preserved by all the operators in the signature of BPA*, and coincide with simulation equivalence and preorder, respectively. In that case, unlike all the other semantics considered in this paper, trace semantics have finite, complete equational axiomatizations over closed terms.

We give a denotational semantics to a calculus λ[otimes ] with overloading and subtyping. In λ[otimes ], the interaction between overloading and subtyping causes self application, and non-normalizing terms exist for each type. Moreover, the semantics of a type depends not on that type alone, but also on infinitely many others. Thus, we need to consider infinitely many domains, which are related by an infinite number of mutually recursive equations. We solve this by considering a functor category from the poset of types modulo equivalence to a category in which each type is interpreted. We introduce a categorical constructor corresponding to overloading, and formalize the equations as a single equation in the functor category. A semantics of λ[otimes ] is then expressed in terms of the minimal solution of this equation. We prove the adequacy theorem for λ[otimes ] following the construction in Pitts (1994) and use it to derive some syntactic properties.

This special issue is devoted to complete and revised versions of papers presented at the Logique et Modèles du Calcul (Logic and Models of Computation) Conference held at CIRM in Marseilles in September 1996.

The conference was organized by Marie-Renée Donnadieu, and the members of the programme committee were Gérard Berry, Jean-Yves Girard, Max Kanovich, Jean-Louis Krivine, Yves Lafont and François Lamarche.

The scope of the conference was quite large, including, for instance, digital circuits, process calculi, abstract machines for lambda-calculus, computational interpretations of linear logic and logical aspects of proof search. Only the last three topics are represented in this special issue of Mathematical Structures in Computer Science, but we think that these papers are quite representative of the liveliness of research in this area on the borderline between mathematics and computing.

We wish to thank Giuseppe Longo, who kindly proposed publishing this issue. For editorial reasons, a few contributions could not be included – they should appear in later issues.

We introduce the notion of strongly concatenable process as a refinement of concatenable processes (Degano et al. 1996), which can be expressed axiomatically via a functor [Qscr ](_) from the category of Petri nets to an appropriate category of symmetric strict monoidal categories, in the precise sense that, for each net N, the strongly concatenable processes of N are isomorphic to the arrows of [Qscr ](N). In addition, we identify a coreflection right adjoint to [Qscr ](_) and characterize its replete image, thus yielding an axiomatization of the category of net computations.

Two operations are presented for a modular approach to the definition of frameworks for rigorous development of software, formally represented as institutions.

The first generalizes models, allowing them to have more structure than the minimum required by their declared signatures, as happens for software modules, which may have local routines that do not appear in their interface.

The second extends sentences, and their interpretation in models, allowing sentences on richer signatures to be used as formulae for poorer ones.

Combining the application of these operations, powerful institutions can be defined, like those for very abstract entities, or for hyper-loose algebraic specifications.

The compatibility of different sequential applications of these operations and properties of the resulting institutions are also studied.

This paper, a revised version of Rutten and Turi (1993), is part of a programme aiming at formulating a mathematical theory of structural operational semantics to complement the established theory of domains and denotational semantics to form a coherent whole (Turi 1996; Turi and Plotkin 1997). The programme is based on a suitable interplay between the induction principle, which pervades modern mathematics, and a dual, non-standard ‘coinduction principle’, which underlies many of the recursive phenomena occurring in computer science.

The aim of the present survey is to show that the elementary categorical notion of a final coalgebra is a suitable foundation for such a coinduction principle. The properties of coalgebraic coinduction are studied both at an abstract categorical level and in some specific categories used in semantics, namely categories of non-well-founded sets, partial orders and metric spaces.

Almost a decade ago, Girard invented linear logic with the notion of a proof-net. Proof-nets are special graphs built from formulas, links and boxes. However, not all nets are proof-nets. First, they must be well constructed (we say that such graphs are proof-structures). Second, a proof-net is a proof-structure that corresponds to a sequential proof. It must satisfy a correctness criterion. One may wonder what this static criterion means for cut-elimination. We prove that every incorrect proof-structure (without cut) can be put in an environment where reductions lead to two kinds of basically wrong configurations: deadlocks and disconnected proof-structures. Thus, this proof says that there does not exist a bigger class of proof-structures than proof-nets where normalization does not lead to obviously bad configurations.

The order-enriched category of monotonic predicate transformers over posets is a model of the refinement calculus of higher order imperative programs and pre-post specifications. This category is shown to be equivalent to the category of spans over ideal relations, and ideal relations are shown to be spans over monotonic functions between posets. To do this we use a skew span construction because the standard categorical span constructions are inapplicable. Axioms are given for products and coproducts of underlying posets as well as the homset as a coexponent, using inequations (for various kinds of lax adjunctions) and conditional equations (for adjunctions in subcategories) that are shown to uniquely determine the structures. The model is described in elementary terms using power allegories, an axiomatic calculus of relations, which makes the proofs accessible to non-specialists and shows that the results generalize to other base categories.

In object-oriented programming, there are many notions of ‘collection with members in X’. This paper offers an axiomatic theory of collections based on monads in the category of sets and total functions. Heuristically, the axioms defining a collection monad state that each collection has a finite set of members of X, that pure 1-element collections exist and that a collection of collections flattens to a single collection whose members are the union of the members of the constituent collections. The relationship between monads and universal algebra leads to a formal definition of collection implementation in terms of tree-processing. Ideas from elementary category theory underly the classification of collections. For example, collections can be zipped if and only if the monad's endofunctor preserves pullbacks. Or, a collection can be uniquely specified by its shape and list of data if the morphisms of the Kleisli category of the monad are all deterministic, and the converse holds for commutative monads. Again, a collection monad is ordered if the monad's functor preserves equalizers of monomorphisms (so, in particular, if collections can be zipped the monad is ordered). Every implementable monad is ordered. It is shown using the well-ordering principle that a collection monad is ordered if and only if its functor admits an appropriated list-valued natural transformation that lists the members of each collection.

We present a formalism of trees with pointers, called abstract Böhm trees, that provide a suitable abstract framework in which various cut-free proofs or normal terms of several λ-calculus based languages (including PCF and Parigot's λμ-calculus) can be faithfully encoded. A simple abstract machine called the View Abstract Machine (VAM) allows us to compute over abstract Böhm trees. The VAM is closely related to Coquand's interaction sequences and debates. The VAM execution over finite abstract Böhm trees always terminates. We next introduce an abstract notion of type that fits the purpose of guaranteeing that the VAM cannot go into deadlock, i.e., that it always reaches a satisfactory final state. Typed abstract Böhm trees can be turned into a category – more naturally a ‘multi-category’ where the domains of arrows are sets of named objects or records. We then go from the abstract to the concrete by giving examples. Our sets of abstract (typed) Böhm trees are relative to an alphabet and a set of types. By instantiating these two parameter sets appropriately, we recover, successively: (η-long) typed Böhm trees; PCF trees as considered in the game models of Hyland–Ong or of Abramsky–Jagadeesan–Malacaria; a notion of classical Böhm tree due to Herbelin that provides a classical version of PCF trees in the style of λμ-calculus; and, finally, cut-free proofs in Novikov's infinitary propositional logic as investigated by Coquand. In a companion paper, we investigate the operational aspects of (untyped) Böhm trees in more depth.

We develop temporal logic from the theory of complete lattices, Galois connections and fixed points. In particular, we prove that all seventeen axioms of Manna and Pnueli's sound and complete proof system for linear temporal logic can be derived from just two postulates, namely that ([oplus ], &[ominus ]tilde;) is a Galois connection and that ([ominus ], [oplus ]) is a perfect Galois connection. We also obtain a similar result for the branching time logic CTL.

A surprising insight is that most of the theory can be developed without the use of negation. In effect, we are studying intuitionistic temporal logic. Several examples of such structures occurring in computer science are given. Finally, we show temporal algebra at work in the derivation of a simple graph-theoretic algorithm.

This paper is tutorial in style and there are no difficult technical results. To the experts in temporal logics, we hope to convey the simplicity and beauty of algebraic reasoning as opposed to the machine-orientedness of logical deduction. To those familiar with the calculational approach to programming, we want to show that their methods extend easily and smoothly to temporal reasoning. For anybody else, this text may serve as a gentle introduction to both areas.

In recent years, the problem of incorporating a set-building type-constructor into a domain theoretic data model has been addressed by different authors. In Jung and Puhlmann (1995) and Puhlmann (1995) we have shown why the so-called snack powerdomain is particularly suitable for modelling a set constructor. We obtain a generalized database model that covers the nested relational model.

While, with the snack powerconstruction, the data structure of domain theoretic databases seems clear, suitable operations for the data model are still to be defined.

In this paper we start this task by defining the operations nest and unnest for the passage between different nesting-levels of the snack powerconstruction. These functions are shown to form an embedding-projection pair, a property that the corresponding functions of nested relational databases do not have. This demonstrates the usefulness of the domain-theoretic approach for modelling databases: for the first time we have operators for re-grouping nested data that respect the idea of an information ordering.

The use of the snack powerdomain leads to fairly complex formulas. To help the reader, illustrations and pictorial interpretations of formulas are given throughout the paper.

We show how to solve the word problem for simply typed λβη-calculus by using a few well-known facts about categories of presheaves and the Yoneda embedding. The formal setting for these results is [Pscr ]-category theory, a version of ordinary category theory where each hom-set is equipped with a partial equivalence relation. The part of [Pscr ]-category theory we develop here is constructive and thus permits extraction of programs from proofs. It is important to stress that in our method we make no use of traditional proof-theoretic or rewriting techniques. To show the robustness of our method, we give an extended treatment for more general λ-theories in the Appendix.

Mixins are modules in which some components are deferred, that is, their definition has to be provided by another module. Moreover, in contrast to parameterized modules (like ML functors), mixin modules can be mutually dependent and their composition supports the redefinition of components (overriding). In this paper, we present a formal model of mixins and their basic composition operators. These operators can be viewed as a kernel language with clean semantics in which one can express more complex operators of existing modular languages, including variants of inheritance in object-oriented programming. Our formal model is given in an ‘institution independent’ way, that is, it is parameterized by the semantic framework modelling the underlying core language.

Interaction nets have proved to be a useful tool for the study of computational aspects of various formalisms (e.g. λ-calculus, term rewriting systems), but they are also a programming paradigm in themselves, and this is actually how they were introduced by Lafont. In this paper we consider semi-simple interaction nets as a programming language, and present a type assignment system using intersection types. First we show that interactions preserve types (i.e., the system enjoys subject reduction), and we compare this type assignment system with the intersection systems for λ-calculus and term rewriting systems. Then we define a recursion scheme that ensures termination of all interaction sequences. By relaxing the scheme and using the type assignment system, we derive another sufficient condition for termination of interaction nets. Finally, we show that although the type system based on general intersection types is not decidable, its restriction to rank 2 types is, and we give an algorithm that computes principal types for nets.

We introduce a natural deduction-like formalisation of Parigot's λμ-calculus. From this, we derive an environment machine that allows any well-typed λμ-term to be reduced to its weak head normal form. The soundness and completeness of the machine is proved.

We give a decision procedure for the extensional equality of total Böhm trees presented by regular systems of recursion equations.