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.

This paper extends the ‘lens’ concept for view updating in Computer Science beyond the categories of sets and ordered sets. It is first shown that a constant complement view updating strategy also corresponds to a lens for a categorical database model. A variation on the lens concept called a c-lens is introduced, and shown to correspond to the categorical notion of Grothendieck opfibration. This variant guarantees a universal solution to the view update problem for functorial update processes.

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 introduce relative formal topology so that we can deal constructively with the closed subsets of a topological space as well as with the open ones. In fact, within standard formal topology, the cover relation allows the definition of the formal opens, which are supposed to act as the formal counterparts of the open subsets, and within balanced formal topology, the binary positivity predicate allows the definition of the formal closed subsets, which are supposed to act as the formal counterparts of the closed subsets. However, these approaches are only fully satisfactory (according to the criterion introduced by the author in Valentini (2005)) if we can provide an adequate formalisation of the cover relation and the positivity predicate. But current formalisations fail in this respect since some intuitionistically valid relations between the open and closed subsets of a concrete topological space cannot be expressed. Our central result is that we can solve this problem through a generalisation of the standard cover relation together with a binary positivity predicate satisfying the positivity axiom.

Consider the first-order theory of a category.d It has a sort of objects, and a sort of arrows (so we may think of it as a small category). We show that, assuming the principle of unique substitutions, the setoids inside a type theoretic universe provide a model for this first-order theory. We also show that the principle of unique substitutions is not derivable in type theory, but that it is strictly weaker than the principle of unique identity proofs.