The pioneering work of Hewitt and Baker on the foundations of concurrency during the seventies has inspired the development of the actor model as a promising object-based framework for understanding open distributed systems. So far, theoretical research on actors has focused on identifying the basic primitives of the model and on characterising the operational behaviour of distributed programming languages in terms of actor components. In this paper, we show that the actor model can also be used as a faithful basis for rigorously designing open distributed systems. We argue that a proof-theoretic approach is better suited to this purpose. An abstract-data-type-like axiomatisation of the actor primitives is proposed to support composing and reasoning from specifications of actor communities within a temporal logical system.

A formulation of lattice theory as a system of rules added to sequent calculus is given. The analysis of proofs for the contraction-free calculus of classical predicate logic known as G3c extends to derivations with the mathematical rules of lattice theory. It is shown that minimal derivations of quantifier-free sequents enjoy a subterm property: all terms in such derivations are terms in the endsequent.

An alternative formulation of lattice theory as a system of rules in natural deduction style is given, both with explicit meet and join constructions and as a relational theory with existence axioms. A subterm property for the latter extends the standard decidable classes of quantificational formulas of pure predicate calculus to lattice theory.

Bloom and Ésik's concept of iteration theory summarises all equational properties that iteration has in common applications, for example, in domain theory, where to every system of recursive equations, the least solution is assigned. This paper shows that in the coalgebraic approach to iteration, the more appropriate concept is that of a functorial iteration theory (called Elgot theory). These theories have a particularly simple axiomatisation, and all well-known examples of iteration theories are functorial. Elgot theories are proved to be monadic over the category of sets in context (or, more generally, the category of finitary endofunctors of a locally finitely presentable category). This demonstrates that functoriality is an equational property from the perspective of sets in context. In contrast, Bloom and Ésik worked in the base category of signatures rather than sets in context, and there iteration theories are monadic but Elgot theories are not. This explains why functoriality was not included in the definition of iteration theories.

We introduce homotopical methods based on rewriting on higher-dimensional categories to prove coherence results in categories with an algebraic structure. We express the coherence problem for (symmetric) monoidal categories as an asphericity problem for a track category and use rewriting methods on polygraphs to solve it. The setting is extended to more general coherence problems, viewed as 3-dimensional word problems in a track category, including the case of braided monoidal categories.

Given an automaton, its behaviour can be modelled as the sets of strings over an alphabet A that can be accepted from any of its states. When considering concurrent systems, we can see a concurrent agent as an automaton, where non-determinism derives from the fact that its states can offer a different behaviour at different moments in time. Non-deterministic computations between a pair of states can then no longer be described as a ‘set’ of strings in a free monoid. Consequently, between two states we will have a labelled structured set of computations, where the structure describes the possibility of two computations parting from each other while maintaining the same observable steps. In this paper, we shall consider different kinds of observation domains and related structured sets of computations. Structured sets of computations will be organised as a category of generalised trees built over a meet-semilattice monoid formalizing the observation domain. Theorems allowing us to introduce the usual concurrency operators in the models and relating different models will then be obtained by first considering ordinary functors (on and between the observation domains), and then lifting them to the categories of structured sets of computations.

In this paper, we investigate the axiomatic semantics of the projection temporal logic programming language MSVL. To this end, we employ Propositional Projection Temporal Logic (PPTL) as an assertion language to specify the desired properties. We give a set of state axioms and state inference rules. In order to deduce a program over an interval, we also formalise a set of rules in terms of a Hoare logic-like triple. These rules enable us to deduce a program into its normal form and from the current state to the next one. They also enable us to verify properties over intervals. In this way, an axiom system for proving the correctness of MSVL programs is established. The axiom system is proved to be sound and relatively complete with respect to an operational model of MSVL, and give an example showing how the axiom system works. Finally, we employ a recently developed prototype verifier based on PVS as an example of semi-automatic verification using MSVL.

A restriction category is an abstract category of partial maps. A Boolean restriction category is a restriction category that supports classical (Boolean) reasoning. Such categories are models of loop-free dynamic logic that is deterministic in the sense that < α > Q ⊂ [α]Q. Classical restriction categories are restriction categories with a locally Boolean structure: it is shown that they are precisely full subcategories of Boolean restriction categories. In particular, a Boolean restriction category may be characterised as a classical restriction category with finite coproducts in which all restriction idempotents split.

Every restriction category admits a restriction embedding into a Boolean restriction category. Thus, every abstract category of partial maps admits a conservative extension that supports classical reasoning. An explicit construction of the classical completion of a restriction category is given.

We give a domain-theoretic analogue of the classical Banach–Alaoglu theorem, showing that the patch topology on the weak$*$ topology is compact. Various theorems follow concerning the stable compactness of spaces of valuations on a topological space. We conclude with reformulations of the patch topology in terms of polar sets or Minkowski functionals, showing, in particular, that the ‘sandwich set’ of linear functionals is compact.

We define what it means for a formal topology to be spatial, and investigate properties related to spatiality both in general and in examples.

We introduce languages of higher-dimensional automata (HDAs) and develop some of their properties. To this end, we define a new category of precubical sets, uniquely naturally isomorphic to the standard one, and introduce a notion of event consistency. HDAs are then finite, labeled, event-consistent precubical sets with distinguished subsets of initial and accepting cells. Their languages are sets of interval orders closed under subsumption; as a major technical step, we expose a bijection between interval orders and a subclass of HDAs. We show that any finite subsumption-closed set of interval orders is the language of an HDA, that languages of HDAs are closed under binary unions and parallel composition, and that bisimilarity implies language equivalence.

It is reasonable to assume that quantum computations take place under the control of the classical world. For modelling this standard situation, we introduce a Classically controlled Quantum Turing Machine (CQTM), which is a Turing machine with a quantum tape for acting on quantum data, and a classical transition function for formalised classical control. In a CQTM, unitary transformations and quantum measurements are allowed. We show that any classical Turing machine can be simulated by a CQTM without loss of efficiency. Furthermore, we show that any $k$-tape CQTM can be simulated by a 2-tape CQTM with a quadratic loss of efficiency. In order to compare CQTMs with existing models of quantum computation, we prove that any uniform family of quantum circuits (Yao 1993) is efficiently approximated by a CQTM. Moreover, we prove that any semi-uniform family of quantum circuits (Nishimura and Ozawa 2002), and any measurement calculus pattern (Danos et al. 2004) are efficiently simulated by a CQTM. Finally, we introduce a Measurement-based Quantum Turing Machine (MQTM), which is a restriction of CQTMs in which only projective measurements are allowed. We prove that any CQTM is efficiently simulated by a MQTM. In order to appreciate the similarity between programming classical Turing machines and programming CQTMs, some examples of CQTMs are given.

In this paper, we investigate several logical frameworks whose expressiveness lies between Conditional Equational Logic and Horn Clause Logic. The main result deals with the PART-construction, which interprets total based algebras as partial algebras. This construction can be viewed as a simulation of Horn Clause Theories by means of Conditional Equational Theories. Other constructions in other frameworks are extendable to simulations in a similar way. The notion of categorical retractive simulation captures some essential properties of these, which allows us to measure the equivalence and difference between institutions.

We explore the way in which the refinement of individual ‘local’ components of a specification relates to the development of a ‘global’ system from a specification of requirements. The observational interpretation of specifications and refinements adds expressive power and flexibility, but introduces some subtle problems. Our study of these issues is carried out in the context of Casl architectural specifications. We introduce a definition of observational equivalence for Casl models, leading to an observational semantics for architectural specifications for which we prove important properties. Overall, this fulfills the long-standing goal of complementing the standard semantics of Casl specifications with an observational view that supports observational refinement of specifications in combination with Casl-style architectural design.

We investigate laws for predicate transformers for the combination of non-deterministic choice and (extended) probabilistic choice, where predicates are taken to be functions to the extended non-negative reals, or to closed intervals of such reals. These predicate transformers correspond to state transformers, which are functions to conical powerdomains, which are the appropriate powerdomains for the combined forms of non-determinism. As with standard powerdomains for non-deterministic choice, these come in three flavours – lower, upper and (order-)convex – so there are also three kinds of predicate transformers. In order to make the connection, the powerdomains are first characterised in terms of relevant classes of functionals.

Much of the development is carried out at an abstract level, a kind of domain-theoretic functional analysis: one considers d-cones, which are dcpos equipped with a module structure over the non-negative extended reals, in place of topological vector spaces. Such a development still needs to be carried out for probabilistic choice per se; it would presumably be necessary to work with a notion of convex space rather than a cone.

We study three comonads derived from the comma construction. The induced coalgebras correspond to the three concepts displayed in the title of the paper. The comonad that yields the *-autonomous categories is, in essence, the Chu construction, which has recently awaken much interest in computer science. We describe its couniversal property. It is right adjoint to the inclusion of *-autonomous categories among autonomous categories, with lax structure-preserving morphisms. Moreover, this inclusion turns out to be comonadic: *-autonomous categories are exactly the Chu-coalgebras.

Priority is a frequently used feature of many computational systems. In this paper we study the expressiveness of two process algebras enriched with different priority mechanisms. In particular, we consider a finite (that is, recursion-free) fragment of asynchronous CCS with global priority (FAP, for short) and Phillips' CPG (CCS with local priority), and contrast their expressive power with that of two non-prioritised calculi, namely the π-calculus and its broadcast-based version, called bπ. We prove, by means of leader-election-based separation results, that, under certain conditions, there exists no encoding of FAP in π-Calculus or CPG. Moreover, we single out another problem in distributed computing, which we call the last man standing problem (LMS for short), that better reveals the gap between the two prioritised calculi above and the two non-prioritised ones, by proving that there exists no parallel-preserving encoding of the prioritised calculi in the non-prioritised calculi retaining any sincere (complete but partially correct, that is, admitting divergence or premature termination) semantics.

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.

We present a systematic study of bisimulation-up-to techniques for coalgebras. This enhances the bisimulation proof method for a large class of state based systems, including labelled transition systems but also stream systems and weighted automata. Our approach allows for compositional reasoning about the soundness of enhancements. Applications include the soundness of bisimulation up to bisimilarity, up to equivalence and up to congruence. All in all, this gives a powerful and modular framework for simplified coinductive proofs of equivalence.

We study equational presentations of functors and monads defined on a category that is equipped by an adjunction F ˧ U : → of descent type. We present a class of functors/monads that admit such an equational presentation that involves finitary signatures in .

We apply these results to an equational description of functors arising in various areas of theoretical computer science.

This paper considers two main aspects of the lower power locale PL(X): first, its relation to the symmetric topos construction of Bunge and Carboni; and second, its points, which, it is shown, are equivalent to the weakly closed sublocales of X with open domain. This is done as part of a more general discussion of arbitrary weakly closed sublocales, including a new characterization using suplattice homomorphisms from o(X) to Sub(1), and a new proof of a theorem of Jibladze relating them to Ω-nuclei.