We introduce convex–concave duality for various models of non-deterministic choice, probabilistic choice and the two of them combined. This complements the well-known duality of stably compact spaces in a pleasing way: convex–concave duality swaps angelic and demonic choice, and leaves probabilistic choice invariant.

We define and investigate a number of small inductively defined classes (idc's), à la Gregorczyk, that are based on argument-bounded initial functions and the bounded minimalisation and bounded counting schemata. We establish equivalences between these and other classes in the literature, with an emphasis on minimalism. We also obtain characterisations of the classes in terms of well-known fragments of first-order predicate logic.

We pose the following question: If a physical experiment were to be completely controlled by an algorithm, what effect would the algorithm have on the physical measurements made possible by the experiment?

In a programme to study the nature of computation possible by physical systems, and by algorithms coupled with physical systems, we have begun to analyse:

1. (i) the algorithmic nature of experimental procedures; and

2. (ii) the idea of using a physical experiment as an oracle to Turing Machines.

Modal and mixed transition systems are specification formalisms that allow the mixing of over- and under-approximation. We discuss three fundamental decision problems for such specifications:

• — whether a set of specifications has a common implementation;

• — whether an individual specification has an implementation; and

• — whether all implementations of an individual specification are implementations of another one.

A defining feature of quantum mechanics is that it allows systems to exist in a superposition of different eigenstates of certain observables such as position or spin. However, superpositions of other quantities such as mass or charge are not seen in nature. It is thought that this disparity is partly due to the fact that it is much easier to carry out interference experiments for certain observables than others. Here we present an interferometry scheme that should allow us to observe interference between the vacuum and a single photon or atom. We begin by presenting a scheme for a Hadamard gate that operates in the Fock state basis and then show how, by creating an interferometer from two such gates, interference between a single particle and the vacuum could indeed be observed. This would provide evidence of a superposition of different particle numbers.

We study the existence of bisimulations for Kleisli morphisms associated with the Giry monad of subprobabilities over Polish spaces. We first investigate these morphisms and show that the problem can be reduced to the existence of bisimulations for objects in the base category of stochastic relations using simulation equivalent congruences. This leads us to a criterion for two objects to be bisimilar.

In this paper we present a semantics-based framework for analysing the quantitative behaviour of programs with respect to resource usage. We start from an operational semantics in which costs are modelled using a dioid structure. The dioid structure of costs allows the definition of the quantitative semantics as a linear operator. We then develop a theory of approximation of such a semantics, which is akin to what is offered by the theory of abstract interpretation for analysing qualitative properties, in order to compute effectively global cost information from the program. We focus on the notion of long-run cost, which models the asymptotic average cost of a program. The abstraction of the semantics has to take two distinct notions of order into account: the order on costs and the order on states. We prove that our abstraction technique provides a correct approximation of the concrete long-run cost of a program.

One natural way to generalise domain theory is to replace partially ordered sets by categories. This kind of generalisation has recently found application in the study of concurrency. An outline is given of the elegant mathematical foundations that have been developed. This is specialised to give a construction of cartesian closed categories of domains, which throws light on standard presentations of domain theory.

We characterise those quasi-metric spaces (X, d) whose poset BX of formal balls satisfies the condition (*) From this characterisation, we then deduce that a quasi-metric space (X, d) is Smyth-complete if and only if BX is a dcpo satisfying condition (*). We also give characterisations in terms of formal balls for sequentially Yoneda complete quasi-metric spaces and for Yoneda complete T1 quasi-metric spaces. Finally, we discuss several properties of the Heckmann quasi-metric on the formal balls of any quasi-metric space.

We prove that the category of -cocomplete separated -categories has bilimits of expanding sequences. This result generalises on various levels the well-known theorem of domain theory that guarantees the existence of bilimits in the category of directed-complete posets and Scott-continuous maps.

Girard's Geometry of Interaction (GoI) develops a mathematical framework for modelling the dynamics of cut elimination. We introduce a typed version of GoI, called Multiobject GoI for both multiplicative linear logic (MLL) and multiplicative exponential linear logic (MELL) with units. We present a categorical setting that includes our previous (untyped) GoI models, as well as more general models based on monoidal *-categories. Our development of multiobject GoI depends on a new theory of partial traces and trace classes, which we believe is of independent interest, as well as an abstract notion of orthogonality (which is related to work of Hyland and Schalk). We develop Girard's original theory of types, data and algorithms in our setting, and show his execution formula to be an invariant of cut elimination (under some restrictions). We prove soundness theorems for the MGoI interpretation (for Multiplicative and Multiplicative Exponential Linear Logic) in partially traced *-categories with an orthogonality. Finally, we briefly discuss the relationship between our GoI interpretation and other categorical interpretations of GoI.

We show that the diamond lattice can be embedded into the Σ02 enumeration degrees preserving 0 and 1, with atoms one high and Π01, and the other one low.

The uniform word problem for finitely presented ortholattices is shown to be solvable through a method of terminating proof search. The axioms of ortholattices are all Harrop formulas, and thus can be expressed in natural deduction style as single succedent rules. A system of natural deduction style rules for orthologic is given as an extension of the system for lattices presented by Negri and von Plato. By considering formal derivations of atomic formulas from a finite number of given atomic formulas, it is shown that proof search is bounded, and thus that the question of derivability of any atomic formula from any finite set of given atomic formulas is decidable.

We consider a variation of the Travelling Salesman Problem (TSP) in which the cities visited have non-zero spatial extent, in contrast with the classical TSP, which has destinations that are mathematical points. This new approach opens up both new analyses of the problem and new algorithms for solutions, while remaining an economic first approximation to the standard problem. We present one particular solution that, depending on the number and size of the cities, can improve existing algorithms solving the classical TSP.

Wang tiles are unit-size squares with coloured edges. In this paper, we approach one aspect of the study of tiling computability: the quest for a universal tile set. Using a complex construction, based on Robinson's classical construction and its different modifications, we build a tile set (pronounced ayin) that almost always simulates any tile set. By way of Banach–Mazur games on tilings topological spaces, we prove that the set of -tilings that do not satisfy the universality condition is meagre in the set of -tilings.

It is well known that many real world networks have a power-law degree distribution (the scale-free property). However, there are no rigorous results for continuous-time quantum walks on such realistic graphs. In this paper, we analyse the space–time behaviour of continuous-time quantum walks and random walks on the threshold network model, which is a reasonable candidate model having the scale-free property. We show that the quantum walker exhibits localisation at the starting point, although the random walker tends to spread uniformly.

This paper provides an abstract definition of a class of logics, called diagrammatic logics, together with a definition of morphisms and 2-morphisms between them. The definition of the 2-category of diagrammatic logics relies on category theory, mainly on adjunction, categories of fractions and limit sketches. This framework is applied to the formalisation of a parameterisation process. This process, which consists of adding a formal parameter to some operations in a given specification, is presented as a morphism of logics. Then the parameter passing process for recovering a model of the given specification from a model of the parameterised specification and an actual parameter is shown to be a 2-morphism of logics.