Semantics of Object Oriented Databases Starting from fundamental structural features of OODBs such as the distinction between values and objects and consequently between types and classes it is argued that the semantics of OODBs can be founded on the semantics of the underlying type system. Given a suitable logic associated with the type system this even comprises object dynamics by a logical characterization of operations (methods). Type systems are considered in a very general sense allowing arbitrary constructors to be defined. If higher-order functions come into play, type semantics can be based on the notion of a topos. In this case the associated logic becomes intuitionistic, but allows classical axiomatic semantics to be generalized.
Towards a better theory of interpretations, or: maybe we need something more general than categories One great advantage of the use of categories in logic, apparent already in Lawvere's thesis, is that it allows for a unified treatment of the concept of an interpretation of one theory into another, and that of a semantics of a theory. In both case what we end up with is a structure-preserving functor, the categorical structure being preserved being "the logic" we are interested in. Until quite recently the categorical structure in question was always decribable in terms of universal properties; in other words it was a set of properties that were obeyed by the relevant categories, as opposed to additional defined structure. Recently new developments in logic and computer science have made the framework above seem too constricted. For example Linear Logic has forced us to consider monoidal categories, which cannot be defined (in general) by universal properties. There are also new kinds of interpretations such that the functors seem to be more than functors, or even monoidal functors. One very telling example is Girard's sytem LC for classical logic. So far all attempts at giving a categorical treatment of it have failed, and we are now sure that the reason for this is that we need something more general than categories to algebraicize this logic. Thus we propose a tentative new framework, which can be tought of as a generalization of multicategories. One interesting thing about it is that the operation of linear negation is always there as a primitive, if only in a purely formal fashion.
Monadic Semantics of CCS-like calculi We start from a calculus as simple as pure CCS and aim at something like the higher-order pi-calculus. In the process several orthogonal issues need to be addressed. As desiderata we would like to have a parametrized semantics, which can deal with different versions of CCS by instantiation of the parameter.
The limit-colimit coincidence in synthetic domain theory In synthetic domain theory one starts off with an ambient category of "sets" (typically a topos) and extracts from it a full subcategory of "well-behaved" sets to act as predomains. In current work, John Longley and I are investigating a notion, which we call well-completeness, that allows a uniform definition of such a subcategory in any realizability topos in which a single axiom holds. The examples include the effective topos, toposes based on domain-theoretic models of the untyped lambda-calculus, and toposes based on partial combinatory algebras of lambda terms. It turns out that the well-complete objects support much of standard domain theory with one important exception: the usual statement of the limit-colimit coincidence fails (both externally - which is hardly surprising - and internally - which is more interesting). However, a suitable (internal) reformulation of the limit-colimit coincidence does hold, and can be used in the usual way to obtain solutions to recursive domain equations as bilimits.
Covariant Types The covariant type system is rich enough to represent polymorphism on inductive types, such as lists and trees, and yet is simple enough to have a set-theoretic semantics. Its chief novelty is to replace function types by transformation types, which denote parametric functions. Their free type variables are all in positive positions, and so can be modelled by covariant functors. They have a simple semantics based on data functors, which can be interpreted in the category of sets.