Domain theoretic models of polymorphism

Thierry Coquand, Carl Gunter, Glynn Winskel

Research output: Contribution to journalArticlepeer-review


We 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. In fact, understanding universal types of the polymorphic λ-calculus as categories of continuous sections appears to be useful generally. For example, the technique also applies to the finitary projection model of Bruce and Longo, and a recent model of Girard. (Indeed the work here was inspired by Girard's and arose through trying to extend the construction of his model to Scott domains). It is hoped that by pin-pointing a key construction this paper will help towards a deeper understanding of models for the polymorphic λ-calculus and the relations between them.

Original languageEnglish (US)
Pages (from-to)123-167
Number of pages45
JournalInformation and Computation
Issue number2
StatePublished - May 1989
Externally publishedYes

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Information Systems
  • Computer Science Applications
  • Computational Theory and Mathematics


Dive into the research topics of 'Domain theoretic models of polymorphism'. Together they form a unique fingerprint.

Cite this