Domain theoretic models of polymorphism

Thierry Coquand, Carl Gunter, Glynn Winskel

Research output: Contribution to journalArticle

Abstract

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
Volume81
Issue number2
DOIs
StatePublished - Jan 1 1989
Externally publishedYes

Fingerprint

Polymorphism
Calculus
Fibration
Model
Category Theory
Projection

ASJC Scopus subject areas

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

Cite this

Domain theoretic models of polymorphism. / Coquand, Thierry; Gunter, Carl; Winskel, Glynn.

In: Information and Computation, Vol. 81, No. 2, 01.01.1989, p. 123-167.

Research output: Contribution to journalArticle

Coquand, Thierry ; Gunter, Carl ; Winskel, Glynn. / Domain theoretic models of polymorphism. In: Information and Computation. 1989 ; Vol. 81, No. 2. pp. 123-167.
@article{0800ae286a794f378f1a6f4b1caedcbd,
title = "Domain theoretic models of polymorphism",
abstract = "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.",
author = "Thierry Coquand and Carl Gunter and Glynn Winskel",
year = "1989",
month = "1",
day = "1",
doi = "10.1016/0890-5401(89)90068-0",
language = "English (US)",
volume = "81",
pages = "123--167",
journal = "Information and Computation",
issn = "0890-5401",
publisher = "Elsevier Inc.",
number = "2",

}

TY - JOUR

T1 - Domain theoretic models of polymorphism

AU - Coquand, Thierry

AU - Gunter, Carl

AU - Winskel, Glynn

PY - 1989/1/1

Y1 - 1989/1/1

N2 - 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.

AB - 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.

UR - http://www.scopus.com/inward/record.url?scp=0024662667&partnerID=8YFLogxK

UR - http://www.scopus.com/inward/citedby.url?scp=0024662667&partnerID=8YFLogxK

U2 - 10.1016/0890-5401(89)90068-0

DO - 10.1016/0890-5401(89)90068-0

M3 - Article

VL - 81

SP - 123

EP - 167

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 2

ER -