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.

In this paper we introduce the notions of nested constraints and application conditions, short nested conditions. For a category associated with a graphical representation such as graphs, conditions are a graphical and intuitive, yet precise, formalism that is well suited to describing structural properties. We show that nested graph conditions are expressively equivalent to first-order graph formulas. A part of the proof includes transformations between two satisfiability notions of conditions, namely -satisfiability and -satisfiability. We consider a number of transformations on conditions that can be composed to construct constraint-guaranteeing and constraint-preserving application conditions, weakest preconditions and strongest postconditions. The restriction of rule applications by conditions can be used to correct transformation systems by pruning transitions leading to states violating given constraints. Weakest preconditions and strongest postconditions can be used to verify the correctness of transformation systems with respect to pre- and postconditions.

We study a measurement-free, untyped λ-calculus with quantum data and classical control. This work arises from previous proposals by Selinger and Valiron, and Van Tonder. We focus on operational and expressiveness issues, rather than (denotational) semantics. We prove subject reduction and confluence, and a standardisation theorem. Moreover, we prove the computational equivalence of the proposed calculus with a suitable class of quantum circuit families.

In this paper we study quasi-metric spaces using domain theory. Our main objective in this paper is to study the maximal point space problem for quasi-metric spaces. Here we prove that quasi-metric spaces that satisfy certain completeness properties, such as Yoneda and Smyth completeness, can be modelled by continuous dcpo's. To achieve this goal, we first study the partially ordered set of formal balls (BX, ⊑) of a quasi-metric space (X, d). Following Edalat and Heckmann, we prove that the order properties of (BX, ⊑) are tightly connected to topological properties of (X, d). In particular, we prove that (BX, ⊑) is a continuous dcpo if (X, d) is algebraic Yoneda complete. Furthermore, we show that this construction gives a model for Smyth-complete quasi-metric spaces. Then, for a given quasi-metric space (X, d), we introduce the partially ordered set of abstract formal balls (BX, ⊑, ≺). We prove that if the conjugate space (X, d−1) of a quasi-metric space (X, d) is right K-complete, then the ideal completion of (BX, ⊑, ≺) is a model for (X, d). This construction provides a model for any Yoneda-complete quasi-metric space (X, d), as well as the Sorgenfrey line, Kofner plane and Michael line.

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 compare three categorical models of type theory with extensional constructs: setoids over extensional type theory; setoids over intensional type theory and a certain free exact category (the free ‘ΠW-pretopos’). By studying the amount of choice available in these categories, we are able show that they are distinct.