Technical reports

Domain theoretic models of polymorphism

Thierry Coquand, Carl Gunter, Glynn Winskel

September 1987, 52 pages

Abstract

The main point of this paper is to give an illustration of a construction useful in producing and describing models of Girard and Reynolds’ polymorphic λ-calculus. The key unifying ideas are that of a Grothendieck fibration and the category of continuous sections associated with it, constructions used in indexed category theory; the universal types of the calculus are interpreted as the category of continuous sections of the fibration. As a major example a new model for the polymorphic λ-calculus is presented. In it a type is interpreted as a Scott domain. The way of understanding universal types of the polymorphic λ-calculus as categories of continuous sections appears to be useful generally, and, as well as applying to the new model introduced here, also applies, for instance, to the retract models of McCracken and Scott, and a recent model of Girard. It is hoped that by pin-pointing a key construction this paper will help towards a deeper understanding of the models for the polymorphic λ-calculus and the relations between them.

Full text

PDF (2.8 MB)

BibTeX record

@TechReport{UCAM-CL-TR-116,
  author =	 {Coquand, Thierry and Gunter, Carl and Winskel, Glynn},
  title = 	 {{Domain theoretic models of polymorphism}},
  year = 	 1987,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-116.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-116},
  number = 	 {UCAM-CL-TR-116}
}