We give a denotational semantics to a calculus λ[otimes ] with overloading and subtyping. In λ[otimes ], the interaction between overloading and subtyping causes self application, and non-normalizing terms exist for each type. Moreover, the semantics of a type depends not on that type alone, but also on infinitely many others. Thus, we need to consider infinitely many domains, which are related by an infinite number of mutually recursive equations. We solve this by considering a functor category from the poset of types modulo equivalence to a category in which each type is interpreted. We introduce a categorical constructor corresponding to overloading, and formalize the equations as a single equation in the functor category. A semantics of λ[otimes ] is then expressed in terms of the minimal solution of this equation. We prove the adequacy theorem for λ[otimes ] following the construction in Pitts (1994) and use it to derive some syntactic properties.

The order-enriched category of monotonic predicate transformers over posets is a model of the refinement calculus of higher order imperative programs and pre-post specifications. This category is shown to be equivalent to the category of spans over ideal relations, and ideal relations are shown to be spans over monotonic functions between posets. To do this we use a skew span construction because the standard categorical span constructions are inapplicable. Axioms are given for products and coproducts of underlying posets as well as the homset as a coexponent, using inequations (for various kinds of lax adjunctions) and conditional equations (for adjunctions in subcategories) that are shown to uniquely determine the structures. The model is described in elementary terms using power allegories, an axiomatic calculus of relations, which makes the proofs accessible to non-specialists and shows that the results generalize to other base categories.

Mixins are modules in which some components are deferred, that is, their definition has to be provided by another module. Moreover, in contrast to parameterized modules (like ML functors), mixin modules can be mutually dependent and their composition supports the redefinition of components (overriding). In this paper, we present a formal model of mixins and their basic composition operators. These operators can be viewed as a kernel language with clean semantics in which one can express more complex operators of existing modular languages, including variants of inheritance in object-oriented programming. Our formal model is given in an ‘institution independent’ way, that is, it is parameterized by the semantic framework modelling the underlying core language.