We continue our study of the negation-free structure of multiplicative linear logic, as represented by the structure of weakly distributive categories, to consider the ‘exponentials’! and ? in the weakly distributive context. In addition to the usual triple and cotriple structure that one would expect on each of the two operators, there must be some connection between them to replace the de Morgan relationship found in the linear logic context. This turns out to be the notion of tensorial strength. We analyze coherence for this situation, using a modification of the usual nets due to Danos, which is a form suitable for linear logic with exponentials but without negation.

Since Pnueli’s seminal paper in 1977, Temporal Logic has been used as a formalism for specifying and verifying the correctness of reactive systems. In this paper, we show that, besides its expressive power, Temporal Logic enjoys a very strong structural property: it is categorical on processes. That is, we show how temporal specifications (as theories) can be embedded in categories of process behaviour, and out of this adjunction we build an institution that is categorical in the sense of Meseguer. This characterisation means that temporal logic is, in a sense, ‘sound and complete’ with respect to process specification and interconnection techniques.

This paper presents several basic results about the non-existence of reflexive objects in cartesian closed topological categories of Hausdorff spaces. In particular, we prove that there are no non-trivial countably compact reflexive objects in the category of Hausdorff k-spaces and, more generally, that any non-trivial reflexive Tychonoff space in this category contains a closed discrete subspace corresponding to a numeral system in the sense of Wadsworth. In addition, we establish that a reflexive Tychonoff space in a cartesian-closed topological category cannot contain a non-trivial continuous image of the unit interval. Therefore, if there exists a non-trivial reflexive Tychonoff space, it does not have a nice geometric structure.

We establish functional completeness of Locally Cartesian Closed Categories by axiomatising the theory of LCCC's in a constructive style. As a consequence we show that there is essentially only one interpretation of Martin-Löf's theory of types with extensional equality in the theory of LCCC's.