Intersection types and bounded quantification are complementary extensions of a first-order programming language with subtyping. We define a typed λ-calculus combining these extensions, illustrate its unusual properties, and develop basic proof-theoretic and semantic results leading to algorithms for subtyping and typechecking.

The reachability semantics for Petri nets can be studied using open Petri nets. For us, an “open” Petri net is one with certain places designated as inputs and outputs via a cospan of sets. We can compose open Petri nets by gluing the outputs of one to the inputs of another. Open Petri nets can be treated as morphisms of a category Open(Petri), which becomes symmetric monoidal under disjoint union. However, since the composite of open Petri nets is defined only up to isomorphism, it is better to treat them as morphisms of a symmetric monoidal double category ${\mathbb O}$ pen(Petri). We describe two forms of semantics for open Petri nets using symmetric monoidal double functors out of ${\mathbb O}$ pen(Petri). The first, an operational semantics, gives for each open Petri net a category whose morphisms are the processes that this net can carry out. This is done in a compositional way, so that these categories can be computed on smaller subnets and then glued together. The second, a reachability semantics, simply says which markings of the outputs can be reached from a given marking of the inputs.

The structure theorem of Joyal, Street and Verity says that every traced monoidal category arises as a monoidal full subcategory of the tortile monoidal category Int. In this paper we focus on a simple observation that a traced monoidal category is closed if and only if the canonical inclusion from into Int has a right adjoint. Thus, every traced monoidal closed category arises as a monoidal co-reflexive full subcategory of a tortile monoidal category. From this, we derive a series of facts for traced models of linear logic, and some for models of fixed-point computation. To make the paper more self-contained, we also include various background results for traced monoidal categories.

Logical relations and their generalisations are a fundamental tool in proving properties of lambda calculi, for example, for yielding sound principles for observational equivalence. We propose a natural notion of logical relations that is able to deal with the monadic types of Moggi's computational lambda calculus. The treatment is categorical, and is based on notions of subsconing, mono factorisation systems and monad morphisms. Our approach has a number of interesting applications, including cases for lambda calculi with non-determinism (where being in a logical relation means being bisimilar), dynamic name creation and probabilistic systems.

Before one can attach a meaning to a sentence, one must distinguish different ways of parsing it. When analysing a language with pregroup grammars, we are thus led to replace the free pregroup by a free compact strict monoidal category. Since a strict monoidal category is a 2-category with one 0-cell, we investigate the free compact 2-category generated by a given category, and describe its 2-cells as labelled transition systems. In particular, we obtain a decision procedure for the equality of 2-cells in the free compact 2-category.

We combine homotopy type theory with axiomatic cohesion, expressing the latter internally with a version of ‘adjoint logic’ in which the discretization and codiscretization modalities are characterized using a judgemental formalism of ‘crisp variables.’ This yields type theories that we call ‘spatial’ and ‘cohesive,’ in which the types can be viewed as having independent topological and homotopical structure. These type theories can then be used to study formally the process by which topology gives rise to homotopy theory (the ‘fundamental ∞-groupoid’ or ‘shape’), disentangling the ‘identifications’ of homotopy type theory from the ‘continuous paths’ of topology. In a further refinement called ‘real-cohesion,’ the shape is determined by continuous maps from the real numbers, as in classical algebraic topology. This enables us to reproduce formally some of the classical applications of homotopy theory to topology. As an example, we prove Brouwer's fixed-point theorem.

A restriction category is an abstract formulation for a category of partial maps, defined in terms of certain specified idempotents called the restriction idempotents. All categories of partial maps are restriction categories; conversely, a restriction category is a category of partial maps if and only if the restriction idempotents split. Restriction categories facilitate reasoning about partial maps as they have a purely algebraic formulation.

In this paper we consider colimits and limits in restriction categories. As the notion of restriction category is not self-dual, we should not expect colimits and limits in restriction categories to behave in the same manner. The notion of colimit in the restriction context is quite straightforward, but limits are more delicate. The suitable notion of limit turns out to be a kind of lax limit, satisfying certain extra properties.

Of particular interest is the behaviour of the coproduct, both by itself and with respect to partial products. We explore various conditions under which the coproducts are ‘extensive’ in the sense that the total category (of the related partial map category) becomes an extensive category. When partial limits are present, they become ordinary limits in the total category. Thus, when the coproducts are extensive we obtain as the total category a lextensive category. This provides, in particular, a description of the extensive completion of a distributive category.

Connections between the sequentiality/concurrency distinction and the semantics of proofs are investigated, with particular reference to games and Linear Logic.

Starting from the $\lambda$-calculus with names, we develop a family of calculi with explicit substitutions that overcome the usual syntactical problems of substitution. The key idea is that only closed substitutions can be moved through certain constructs. This gives a weak form of reduction, called closed reduction, which is rich enough to capture both the call-by-value and call-by-name evaluation strategies in the $\lambda$-calculus. Moreover, since substitutions can move through abstractions and reductions are allowed under abstractions (if certain conditions hold), closed reduction naturally provides an efficient notion of reduction with a high degree of sharing and low overheads. We present a family of abstract machines for closed reduction. Our benchmarks show that closed reduction performs better than all standard weak strategies, and its low overheads make it more efficient than optimal reduction in many cases.

We extend the theory of labelled Markov processes to include internal non-determinism, which is a fundamental concept for the further development of a process theory with abstraction on non-deterministic continuous probabilistic systems. We define non-deterministic labelled Markov processes (NLMP) and provide three definitions of bisimulations: a bisimulation following a traditional characterisation; a state-based bisimulation tailored to our ‘measurable’ non-determinism; and an event-based bisimulation. We show the relations between them, including the fact that the largest state bisimulation is also an event bisimulation. We also introduce a variation of the Hennessy–Milner logic that characterises event bisimulation and is sound with respect to the other bisimulations for an arbitrary NLMP. This logic, however, is infinitary as it contains a denumerable . We then introduce a finitary sublogic that characterises all bisimulations for an image finite NLMP whose underlying measure space is also analytic. Hence, in this setting, all the notions of bisimulation we consider turn out to be equal. Finally, we show that all these bisimulation notions are different in the general case. The counterexamples that separate them turn out to be non-probabilistic NLMPs.

In this paper, we propose an approach to quantum λ-calculi. The ‘quantum data-classical control’ paradigm is considered. Starting from a measurement-free untyped quantum λ-calculus called Q, we will study standard properties such as confluence and subject reduction, and some good quantum properties. We will focus on the expressive power, analysing the relationship with other quantum computational models. Successively, we will add an explicit measurement operator to Q. On the resulting calculus, called Q*, we will propose a complete study of reduction sequences regardless of their finiteness, proving confluence results. Moreover, since the stronger motivation behind quantum computing is the research of new results in computational complexity, we will also propose a calculus which captures the three classes of quantum polytime complexity, showing an ICC-like approach in the quantum setting.

A topological space X is called well-filtered if for any filtered family $\mathcal{F}$ of compact saturated sets and an open set U, ∩ $\mathcal{F}$ ⊆ U implies F ⊆ U for some F ∈ $\mathcal{F}$. Every sober space is well-filtered and the converse is not true. A dcpo (directed complete poset) is called well-filtered if its Scott space is well-filtered. In 1991, Heckmann asked whether every UK-admitting (the same as well-filtered) dcpo is sober. In 2001, Kou constructed a counterexample to give a negative answer. In this paper, for each T1 space X we consider a dcpo D(X) whose maximal point space is homeomorphic to X and prove that X is well-filtered if and only if D(X) is well-filtered. The main result proved here enables us to construct new well-filtered dcpos that are not sober (only one such example is known by now). A space will be called K-closed if the intersection of every filtered family of compact saturated sets is compact. Every well-filtered space is K-closed. Some similar results on K-closed spaces are also proved.

In this paper we consider Milner's calculus CCS enriched by a probabilistic choice operator. The calculus is given operational semantics based on probabilistic transition systems. We define operational notions of preorder and equivalence as probabilistic extensions of the simulation preorder and the bisimulation equivalence respectively. We extend existing category-theoretic techniques for solving domain equations to the probabilistic case and give two denotational semantics for the calculus. The first, ‘smooth’, semantic model arises as a solution of a domain equation involving the probabilistic powerdomain and solved in the category CONT⊥ of continuous domains. The second model also involves an appropriately restricted probabilistic powerdomain, but is constructed in the category CUM of complete ultra-metric spaces, and hence is necessarily ‘discrete’. We show that the domain-theoretic semantics is fully abstract with respect to the simulation preorder, and that the metric semantics is fully abstract with respect to bisimulation.

We consider the Pure Safe Ambient Calculus, which is Levi and Sangiorgi's Safe Ambient Calculus (a variant of Cardelli and Gordon's Mobile Ambient Calculus) restricted to its mobility primitives – in particular, we focus on its expressive power. Since it has no form of communication or substitution, we show how these notions can be simulated by mobility and modifications in the hierarchical structure of ambients. As a main result, we use these techniques to design an encoding of the synchronous $\pi$-calculus into pure ambients, and we study its correctness, thus showing that pure ambients are as expressive as the $\pi$-calculus. In order to simplify the proof and give an intuitive understanding of the encoding, we design an intermediate language, the $\pi$-Calculus with Explicit Substitutions and Channels, which is an extension of the $\pi$-calculus in which communication and substitution are broken into simpler steps, and we show that is has the same expressive power as the $\pi$-calculus.

A purely syntactic and untyped variant of Normalisation by Evaluation for the $\lambda$-calculus is presented in the framework of a two-level $\lambda$-calculus with rewrite rules to model the inverse of the evaluation functional. Among its operational properties there is a standardisation theorem that formally establishes the adequacy of implementation in functional programming languages. An example implementation in Haskell is provided. The relation to the usual type-directed Normalisation by Evaluation is highlighted, using a short analysis of $\eta$-expansion that leads to a perspicuous strong normalisation and confluence proof for $\beta\eta\!\up$-reduction as a byproduct.

The connections between formal topology and domain theory are surveyed and various types of continuous domains are represented as formal spaces through locally Stone and locally Scott formal topologies.

We propose a uniform way of isolating a subcategory of predomains within the category of modest sets determined by a partial combinatory algebra (PCA). Given a divergence on a PCA (which determines a notion of partiality), we identify a candidate category of predomains, the well-complete objects. We show that, whenever a single strong completeness axiom holds, the category satisfies appropriate closure properties. We consider a range of examples of PCAs with associated divergences and show that in each case the axiom does hold. These examples encompass models allowing a ‘parallel’ style of computation (for example, by interleaving), as well as models that seemingly allow only ‘sequential’ computation, such as those based on term-models for the lambda-calculus. Thus, our approach provides a uniform approach to domain theory across a wide class of realizability models. We compare our treatment with previous approaches to domain theory in realizability models. It appears that no other approach applies across such a wide range of models.

We use a syntactical notion of Kripke models to obtain interpretations of subsystems of arithmetic in their intuitionistic counterparts. This yields, in particular, a new proof of Buss' result that the Skolem functions of Bounded Arithmetic are polynomial time computable.

The study of isomorphisms of types has, in the main, been carried out in an intuitionistic setting. We extend some of this work to classical logic for both call-by-name and call-by-value computations by means of polarised linear logic and game semantics. This leads to equational characterisations of these isomorphisms for all the propositional connectives.

Linear logical frameworks with subexponentials have been used for the specification of, among other systems, proof systems, concurrent programming languages and linear authorisation logics. In these frameworks, subexponentials can be configured to allow or not for the application of the contraction and weakening rules while the exchange rule can always be applied. This means that formulae in such frameworks can only be organised as sets and multisets of formulae not being possible to organise formulae as lists of formulae. This paper investigates the proof theory of linear logic proof systems in the non-commutative variant. These systems can disallow the application of exchange rule on some subexponentials. We investigate conditions for when cut elimination is admissible in the presence of non-commutative subexponentials, investigating the interaction of the exchange rule with the local and non-local contraction rules. We also obtain some new undecidability and decidability results on non-commutative linear logic with subexponentials.