Technical reports

DI-domains as a model of polymorphism

Thierry Coquand, Carl Gunter, Glynn Winskel

May 1987, 19 pages

DOI: 10.48456/tr-107

Abstract

This paper investigates a model of the polymorphic lambda calculus recently described by Girard (1985). This model differs from earlier ones in that all the types are interpreted as domains rather than closures or finitary projections on a universal domain. The objective in this paper is to generalize Girard’s construction to a larger category called dI-domains, and secondly to show how Girard’s construction (and this generalization) can be done abstractly. It demonstrates that the generalized construction can be used to do denotational semantics in the ordinary way, but with the added feature of type polymorphism.

Full text

PDF (0.8 MB)

BibTeX record

@TechReport{UCAM-CL-TR-107,
  author =	 {Coquand, Thierry and Gunter, Carl and Winskel, Glynn},
  title = 	 {{DI-domains as a model of polymorphism}},
  year = 	 1987,
  month = 	 may,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-107.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-107},
  number = 	 {UCAM-CL-TR-107}
}