The purpose of this paper is to develop the basic theory of stably compact spaces (viz. compact, locally compact, coherent sober spaces) and introduce in an accessible manner and with a minimum of prerequisites some significant new lines of investigation and application arising from recent research, which has arisen primarily in the theoretical computer science community. Three primary themes have developed:

1. (i) the property of stable compactness is preserved under a large variety of constructions involving powerdomains, hyperspaces and function spaces;

2. (ii) the underlying de Groot duality of stably compact spaces, which finds varied expression, is reflected by duality theorems involving the just mentioned constructions; and

3. (iii) the notion of inner and outer pavings is a useful and natural tool for such studies of stably compact spaces.

Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively defined datatypes such as finite lists, finite trees and the natural numbers. Coinduction is the dual principle that can be used to reason about coinductive datatypes such as infinite streams or trees, but it is not as widespread or as well understood. In this paper, we illustrate through several examples the use of coinduction in informal mathematical arguments. Our aim is to promote the principle as a useful tool for the working mathematician and to bring it to a level of familiarity on par with induction. We show that coinduction is not only about bisimilarity and equality of behaviors, but also applicable to a variety of functions and relations defined on coinductive datatypes.

In this paper we develop novel quantum algorithms based on Quantum Multi-Object Search (QMOS) for convex hulls and general object intersection reporting, with applications to computer graphics. These algorithms are developed and described using standard concepts from computer science by encapsulating the physics of quantum computation within black-box subroutines.

In another paper (Abramsky et al. 1999), we have developed Abramsky's analysis of Girard's Geometry of Interaction programme in detail. In this paper, our goal is to study the data ow based computational aspects of that analysis. We introduce unique decomposition categories that provide a suitable categorical framework for such computational analysis. The current study also serves to establish connections with the work on proof nets and paths by Girard and Danos and Regnier in this categorical setting. The latter goal is partially achieved here by the presentation of categorical models for dynamic algebras.

Computability has its origins in Logic within the framework formed along the original path laid down by the founding fathers of the modern foundational analysis for Mathematics (Frege and Hilbert). This theoretical itinerary, which was largely focused on Logic and Arithmetic, departed in principle from the renewed relations between Geometry and Physics occurring at the time. In particular, the key issue of physical measurement, as our only access to ‘reality’, played no part in its theoretical framework. This is in stark contrast to the position in Physics, where the role of measurement has been a core theoretical and epistemological issue since Poincaré, Planck and Einstein. Furthermore, measurement is intimately related to unpredictability, (in-)determinism and the relationship with physical space–time. Computability, despite having exact access to its own discrete data type, provides a unique tool for the investigation of ‘unpredictability’ in both Physics and Biology through its fine-grained analysis of undecidability – note that unpredictability coincides with physical randomness in both classical and quantum frames. Moreover, it now turns out that an understanding of randomness in Physics and Biology is a key component of the intelligibility of Nature. In this paper, we will discuss a few results following along this line of thought.

This article proposes a global escape mechanism which can handle unexpected or unwanted conditions changing the default execution of distributed communicational flows, preserving compatibility of the multiparty conversations. Our escape is realized by a collection of asynchronous local exceptions which can be thrown at any stage of the communication and to any subsets of participants in a multiparty session. This flexibility enables to model complex exceptions such as criss-crossing global interactions and error handling for distributed cooperating threads. Guided by multiparty session types, our semantics is proven to provide a termination algorithm for global escapes. Our type system guarantees further safety and liveness properties, such as progress within the session and atomicity of escapes with respect to the subset of involved participants.

In the distributed Deutsch–Jozsa promise problem, two parties are to determine whether their respective strings x, y ∈ {0,1}n are at the Hamming distanceH(x, y) = 0 or H(x, y) = $\frac{n}{2}$. Buhrman et al. (STOC' 98) proved that the exact quantum communication complexity of this problem is O(log n) while the deterministic communication complexity is Ω(n). This was the first impressive (exponential) gap between quantum and classical communication complexity. In this paper, we generalize the above distributed Deutsch–Jozsa promise problem to determine, for any fixed $\frac{n}{2}$ ⩽ k ⩽ n, whether H(x, y) = 0 or H(x, y) = k, and show that an exponential gap between exact quantum and deterministic communication complexity still holds if k is an even such that $\frac{1}{2}$n ⩽ k < (1 − λ)n, where 0 < λ < $\frac{1}{2}$ is given. We also deal with a promise version of the well-known disjointness problem and show also that for this promise problem there exists an exponential gap between quantum (and also probabilistic) communication complexity and deterministic communication complexity of the promise version of such a disjointness problem. Finally, some applications to quantum, probabilistic and deterministic finite automata of the results obtained are demonstrated.

The Coq system is a Curry–Howard based proof assistant. Therefore, it contains a full functional, strongly typed programming language, which can be used to enhance the system with powerful automation tools through the implementation of reflexive tactics. We present the implementation of a cylindrical algebraic decomposition algorithm within the Coq system, whose certification leads to a proof producing decision procedure for the first-order theory of real numbers.

The notion of a natural model of type theory is defined in terms of that of a representable natural transfomation of presheaves. It is shown that such models agree exactly with the concept of a category with families in the sense of Dybjer, which can be regarded as an algebraic formulation of type theory. We determine conditions for such models to satisfy the inference rules for dependent sums Σ, dependent products Π and intensional identity types Id, as used in homotopy type theory. It is then shown that a category admits such a model if it has a class of maps that behave like the abstract fibrations in axiomatic homotopy theory: They should be stable under pullback, closed under composition and relative products, and there should be weakly orthogonal factorizations into the class. It follows that many familiar settings for homotopy theory also admit natural models of the basic system of homotopy type theory.

There are two main approaches to obtaining ‘topological’ cartesian-closed categories. Under one approach, one restricts to a full subcategory of topological spaces that happens to be cartesian closed – for example, the category of sequential spaces. Under the other, one generalises the notion of space – for example, to Scott's notion of equilogical space. In this paper, we show that the two approaches are equivalent for a large class of objects. We first observe that the category of countably based equilogical spaces has, in a precisely defined sense, a largest full subcategory that can be simultaneously viewed as a full subcategory of topological spaces. In fact, this category turns out to be equivalent to the category of all quotient spaces of countably based topological spaces. We show that the category is bicartesian closed with its structure inherited, on the one hand, from the category of sequential spaces, and, on the other, from the category of equilogical spaces. We also show that the category of countably based equilogical spaces has a larger full subcategory that can be simultaneously viewed as a full subcategory of limit spaces. This full subcategory is locally cartesian closed and the embeddings into limit spaces and countably based equilogical spaces preserve this structure. We observe that it seems essential to go beyond the realm of topological spaces to achieve this result.

We investigate Girard's calculus Fω as a ‘Curry style’ type assignment system for pure lambda terms. First we show an example of a strongly normalizable term that is untypable in Fω. Then we prove that every partial recursive function is nonuniformly represented in Fω (even if quantification is restricted to constructor variables of level 1). It follows that the type reconstruction problem is undecidable and cannot be recursively separated from normalization.

This paper focusses on the determination of the dihomotopy classes of dipaths in cubical complexes, representing the essentially different computations in a given concurrent program due to different schedules. Several new notions have to be developed, for example, the domains of dependence (Definition 2.4), which are borrowed from relativity theory (Penrose 1972). However, it turns out that the algorithm determining deadlocks and unsafe regions described in Fajstrup et al. (1998a; 1998b) can be modified and applied to do the essential calculational work.

An approach to point-free geometry based on the notion of a quasi-metric is proposed in which the primitives are the regions and a non-symmetric distance between regions. The intended models are the bounded regular closed subsets of a metric space together with the Hausdorff excess measure.

The notion of a recognizable set of words, trees or graphs is relative to an algebraic structure on the set of words, trees or graphs respectively. We establish that several algebraic structures yield the same notion of a recognizable set of graphs. This notion is equivalent to that of a fully cutset-regular set of graphs introduced by Fellows and Abrahamson. We also establish that the class of recognizable sets of graphs is closed under the operations considered in these various equivalent definitions. This fact is not a standard consequence of the definition of recognizability.

We propose compactly generated monotone convergence spaces as a well-behaved topological generalisation of directed-complete partial orders (dcpos). The category of such spaces enjoys the usual properties of categories of ‘predomains’ in denotational semantics. Moreover, such properties are retained if one restricts to spaces with a countable pseudobase in the sense of E. Michael, a fact that permits connections to be made with computability theory, realizability semantics and recent work on the closure properties of topological quotients of countably based spaces (qcb spaces). We compare the standard domain-theoretic constructions of products and function spaces on dcpos with their compactly generated counterparts, showing that these agree in important cases, though not in general.

We introduce Horn linear logic as a comprehensive logical system capable of handling the typical AI problem of making a plan of the actions to be performed by a robot so that he could get into a set of final situations, if he started with a certain initial situation. Contrary to undecidability of propositional Horn linear logic, the planning problem is proved to be decidable for a reasonably wide class of natural robot systems.

The planning problem is proved to be EXPTIME-complete for the robot systems that allow actions with non-deterministic effects. Fixing a finite signature, that is a finite set of predicates and their finite domains, we get a polynomial time procedure of making plans for the robot system over this signature.

The planning complexity is reduced to PSPACE for the robot systems with only pure deterministic actions.

As honest numerical parameters in our algorithms we invoke the length of description of a planning task ‘from W to Z˜’ and the Kolmogorov descriptive complexity of AxT, a set of possible actions.

The purpose of this short paper is to sketch the development of a few basic topics in the history of realizability. The number of topics is quite limited and reflects very much my own personal taste, prejudices and area of competence.

We present a realisability model for a call-by-value, higher-order programming language with parametric polymorphism, general first-class references, and recursive types. The main novelty is a relational interpretation of open types that include general reference types. The interpretation uses a new approach to modelling references.

The universe of semantic types consists of world-indexed families of logical relations over a universal predomain. In order to model general reference types, worlds are finite maps from locations to semantic types: this introduces a circularity between semantic types and worlds that precludes a direct definition of either. Our solution is to solve a recursive equation in an appropriate category of metric spaces. In effect, types are interpreted using a Kripke logical relation over a recursively defined set of worlds.

We illustrate how the model can be used to prove simple equivalences between different implementations of imperative abstract data types.

Light affine logic is a variant of linear logic with a polynomial cut-elimination procedure. We study the extensional expressive power of light affine logic with respect to a general notion of encoding of functions in the setting of the Curry–Howard correspondence. We consider light affine logic with both fixpoints of formulae and second-order quantifiers, and analyse the properties of polytime soundness and polytime completeness for various fragments of this system. In particular, we show that the implicative propositional fragment is not polytime complete if we place some reasonable conditions on the encodings. Following previous work, we show that second order leads to polytime unsoundness. We then introduce simple constraints on second-order quantification and fixpoints, and prove that the fragments obtained are polytime sound and complete.

Two imperative programming language phrases interfere when one writes to a storage variable that the other reads from or writes to. Reynolds has described an elegant linguistic approach to controlling interference in which a refinement of typed λ-calculus is used to limit sharing of storage variables; in particular, different identifiers are required never to interfere. This paper examines semantic foundations of the approach.

We describe a category that has (an abstraction of) interference information built into all objects and maps. This information is used to define a ‘tensor’ product whose components are required never to interfere. Environments are defined using the tensor, and procedure types are obtained via a suitable adjunction. The category is a model of intuitionistic linear logic. Reynolds' concept of passive type - i.e. types for phrases that do not write to any storage variables - is shown to be closely related, in this model, to Girard's ‘of course’ modality.