dI-domains as a model of polymorphism

Abstract

In this paper we investigate a model construction recently described by Jean Yves Girard. This model differs from the models of McCracken, Scott, etc. in that the types are interpreted (quite pleasingly) as domains rather than closures or finitary projections on a universal domain. Our objective in this paper is two-fold. First, we would like to generalize Girard's construction to a larger category called dI-domains which was introduced by Berry [2]. The dI-domains possess many of the virtues of the domains used by Girard. Moreover, the dI-domains are closed under the separated sum and lifting operators from denotational semantics and this is not true of the domains of Girard. We intend to demonstrate that our generalized construction can be used to do denotational semantics in the ordinary way, but with the added feature of type polymorphism with a “types as domains” interpretation. Our second objective is to show how Girard's construction (and our generalization) can be done abstractly. We also give a representational description of our own construction using the notion of a prime event structure.