### 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 language | English (US) |
---|---|

Pages (from-to) | 123-167 |

Number of pages | 45 |

Journal | Information and Computation |

Volume | 81 |

Issue number | 2 |

DOIs | |

State | Published - May 1989 |

Externally published | Yes |

### Fingerprint

### ASJC Scopus subject areas

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

### Cite this

*Information and Computation*,

*81*(2), 123-167. https://doi.org/10.1016/0890-5401(89)90068-0

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

Research output: Contribution to journal › Article

*Information and Computation*, vol. 81, no. 2, pp. 123-167. https://doi.org/10.1016/0890-5401(89)90068-0

}

TY - JOUR

T1 - Domain theoretic models of polymorphism

AU - Coquand, Thierry

AU - Gunter, Carl

AU - Winskel, Glynn

PY - 1989/5

Y1 - 1989/5

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

AN - SCOPUS:0024662667

VL - 81

SP - 123

EP - 167

JO - Information and Computation

JF - Information and Computation

SN - 0890-5401

IS - 2

ER -