TY - GEN
T1 - dI-domains as a model of polymorphism
AU - Coquand, Thierry
AU - Gunter, Carl
AU - Winskel, Glynn
N1 - Publisher Copyright:
© 1988, Springer-Verlag.
PY - 1988
Y1 - 1988
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85029628159&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85029628159&partnerID=8YFLogxK
U2 - 10.1007/3-540-19020-1_18
DO - 10.1007/3-540-19020-1_18
M3 - Conference contribution
AN - SCOPUS:85029628159
SN - 9783540190202
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 344
EP - 363
BT - Mathematical Foundations of Programming Language Semantics - 3rd Workshop, Proceedings
A2 - Main, Michael
A2 - Melton, Austin
A2 - Schmidt, David
A2 - Mislove, Michael
PB - Springer
T2 - 3rd Workshop on the Mathematical Foundations of Programming Language Semantics, 1987
Y2 - 8 April 1987 through 10 April 1987
ER -