We study computably enumerable (c.e.) prefix codes that are capable of coding all positive integers in an optimal way up to a fixed constant: these codes will be called universal. We prove various characterisations of these codes, including the following one: a c.e. prefix code is universal if and only if it contains the domain of a universal self-delimiting Turing machine. Finally, we study various properties of these codes from the points of view of computability, maximality and density.

We analyse the reduction of differential interaction nets from the point of view of so-called ‘true concurrency,’ that is, employing a non-interleaving model of parallelism. More precisely, we associate with each differential interaction net an event structure describing its reduction. We show how differential interaction nets are only able to generate confusion-free event structures, and we argue that this is a serious limitation in terms of the concurrent behaviours they may express. In fact, confusion is an extremely elementary phenomenon in concurrency (for example, it already appears in CCS with just prefixing and parallel composition) and we show how its presence is preserved by any encoding respecting the degree of distribution and the reduction semantics. We thus infer that no reasonably expressive process calculus may be satisfactorily encoded in differential interaction nets. We conclude with an analysis of one such encoding proposed by Ehrhard and Laurent, and argue that it does not contradict our claims, but rather supports them.

We propose a variant of public announcement logic for asynchronous systems. To capture asynchrony, we introduce two different modal operators for sending and receiving messages. The natural approach to defining the semantics leads to a circular definition, but we describe two restricted cases in which we solve this problem. The first case requires the Kripke model representing the initial epistemic situation to be a finite tree, and the second one only allows announcements from the existential fragment. After establishing some validities, we study the model checking problem and the satisfiability problem in cases where the semantics is well-defined, and we provide several complexity results.

This paper contributes a feedback operator, in the form of a monoidal trace, to the theory of coalgebraic, state-based modelling of components. The feedback operator on components is shown to satisfy the trace axioms of Joyal, Street and Verity. We employ McCurdy's tube diagrams, which are an extension of standard string diagrams for monoidal categories, to represent and manipulate component diagrams. The microcosm principle then yields a canonical ‘inner’ traced monoidal structure on the category of resumptions (elements of final coalgebras/components). This generalises an observation by Abramsky, Haghverdi and Scott.

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.

Since the publication of the paper Carboni and Johnstone (1995), we have become aware of two independent errors in it. Although neither of them has any effect on the main results of the paper, concerning when a category obtained by Artin glueing is a topos, we feel it is appropriate to publish this correction in the hope that it may prevent future readers of Carboni and Johnstone (1995) from being misled. We are grateful to Tom Leinster and to Marek Zawadowski for drawing our attention to the two errors.

The first part of the paper presents a generalization of the well-known Baire category theorem. The generalization consists in replacing the dense open sets of the original formulation by dense UCO sets, where UCO means union of closed and open. This topological theorem is exactly what is needed to prove in the second part of the paper the locale-theoretic result that locales whose frame of opens has a countable presentation (countably many generators and countably many relations) are spatial. This spatiality theorem does not require choice.

Continuous lattices were characterised by Martín Escardó as precisely those objects that are Kan-injective with respect to a certain class of morphisms. In this paper we study Kan-injectivity in general categories enriched in posets. As an example, ω-CPO's are precisely the posets that are Kan-injective with respect to the embeddings ω ↪ ω + 1 and 0 ↪ 1.

For every class $\mathcal{H}$ of morphisms, we study the subcategory of all objects that are Kan-injective with respect to $\mathcal{H}$ and all morphisms preserving Kan extensions. For categories such as Top0 and Pos, we prove that whenever $\mathcal{H}$ is a set of morphisms, the above subcategory is monadic, and the monad it creates is a Kock–Zöberlein monad. However, this does not generalise to proper classes, and we present a class of continuous mappings in Top0 for which Kan-injectivity does not yield a monadic category.

It is an empirical observation arising from the study of higher type computability that a wide range of approaches to defining a class of (hereditarily) total functionals over leads in practice to a relatively small handful of distinct type structures. Among these are the type structure C of Kleene–Kreisel continuous functionals, its effective substructure Ceff and the type structure HEO of the hereditarily effective operations. However, the proofs of the relevant equivalences are often non-trivial, and it is not immediately clear why these particular type structures should arise so ubiquitously.

In this paper we present some new results that go some way towards explaining this phenomenon. Our results show that a large class of extensional collapse constructions always give rise to C, Ceff or HEO (as appropriate). We obtain versions of our results for both the ‘standard’ and ‘modified’ extensional collapse constructions. The proofs make essential use of a technique due to Normann.

Many new results, as well as some previously known ones, can be obtained as instances of our theorems, but more importantly, the proofs apply uniformly to a whole family of constructions, and provide strong evidence that the three type structures under consideration are highly canonical mathematical objects.

In this paper we prove that any Turing machine that uses only a finite computational space for every input cannot solve an uncomputable problem even when it runs in accelerated mode. We also propose two ways to define the language accepted by an accelerated Turing machine. Accordingly, the classes of languages accepted by accelerated Turing machines are the closure under Boolean operations of the sets Σ1 and Σ2.

Computational indistinguishability is a notion in complexity-theoretic cryptography and is used to define many security criteria. However, in traditional cryptography, proving computational indistinguishability is usually informal and becomes error-prone when cryptographic constructions are complex. This paper presents a formal proof system based on an extension of Hofmann's SLR language, which can capture probabilistic polynomial-time computations through typing and is sufficient for expressing cryptographic constructions. In particular, we define rules that directly justify the computational indistinguishability between programs, and then prove that these rules are sound with respect to the set-theoretic semantics, and thus the standard definition of security. We also show that it is applicable in cryptography by verifying, in our proof system, Goldreich and Micali's construction of a pseudorandom generator, and the equivalence between next-bit unpredictability and pseudorandomness.

We build a logical system named a conjunctive sequent calculus which is a conjunctive fragment of the classical propositional sequent calculus in the sense of proof theory. We prove that a special class of formulae of a consistent conjunctive sequent calculus forms a bounded complete continuous domain without greatest element (for short, a proper BC domain), and each proper BC domain can be obtained in this way. More generally, we present conjunctive consequence relations as morphisms between consistent conjunctive sequent calculi and build a category which is equivalent to that of proper BC domains with Scott-continuous functions. A logical characterization of purely syntactic form for proper BC domains is obtained.

Algebraic CPOs naturally generalize to finitely accessible categories, and Scott domains (i.e., consistently complete algebraic CPOs) then correspond to what we call Scott-complete categories: finitely accessible, consistently (co-)complete categories. We prove that the category SCC of all Scott-complete categories and all continuous functors is cartesian closed and provides fixed points for a large collection of endofunctors. Thus, SCC can serve as a basis for semantics of computer languages.

We give a logic-independent semantics for predefined (data) types within the categorical abstract model theoretic framework of the theory of institutions. We develop a generic interpolation result for this semantics, which can be easily applied to various concrete situations from the theory and practice of specification and programming. Our study of interpolation is motivated by a number of important applications to computing science, especially in the area of structured specifications.

We show that the extensional ordering of the sequential functionals of pure type 3, for example, as defined via game semantics (Abramsky et al. 1994; Hyland and Ong 2000), is not cpo-enriched. This shows that this model does not equal Milner's (Milner 1977) fully abstract model for PCF.

The last years have seen an increasing interest in classifying (existence claims in) classical mathematical theorems according to their strength. We pursue this goal from the refined perspective of computational complexity. Specifically, we establish that rigorously solving the Dirichlet Problem for Poisson's Equation is in a precise sense ‘complete’ for the complexity class ${\#\mathcal{P}}$ and thus as hard or easy as parametric Riemann integration (Friedman 1984; Ko 1991. Complexity Theory of Real Functions).

This paper is part of a general programme of treating explicit substitutions as the primary λ-calculi from the point of view of foundations as well as applications. We work in a composition-free calculus of explicit substitutions and an augmented calculus obtained by adding explicit garbage-collection, and explore the relationship between intersection-types and reduction.

We show that the terms that normalise by leftmost reduction and the terms that normalise by head reduction can each be characterised as the terms typable in a certain system. The relationship between typability and strong normalisation is subtly different from the classical case: we show that typable terms are strongly normalising but give a counterexample to the converse. Our notions of leftmost and head reduction are non-deterministic, and our normalisation theorems apply to any computations obeying these strategies. In this way we refine and strengthen the classical normalisation theorems. The proofs require some new techniques in the presence of reductions involving explicit substitutions. Indeed, our proofs do not rely on results from classical λ-calculus, which in our view is subordinate to the calculus of explicit substitution.

We show that the disintegration operator on a complete separable metric space along a projection map, restricted to measures for which there is a unique continuous disintegration, is strongly Weihrauch equivalent to the limit operator Lim. When a measure does not have a unique continuous disintegration, we may still obtain a disintegration when some basis of continuity sets has the Vitali covering property with respect to the measure; the disintegration, however, may depend on the choice of sets. We show that, when the basis is computable, the resulting disintegration is strongly Weihrauch reducible to Lim, and further exhibit a single distribution realizing this upper bound.

Multirelational semantics are well suited to reasoning about programs involving two kinds of non-determinism. This paper lays the categorical foundations for an algebraic calculus of multirelations.

A notion of bilattice was first proposed by Ginsberg as a general framework for many applications. Related notions were further investigated and applied for various goals by Fitting. In the present paper a general definition of bilattices is proposed, which covers all particular cases that have actually been used in the literature. It is shown also that in the finite case every bilattice in our sense is graphically representable by a special type of a two-dimensional diagram.