Abstract
A new general notion of model for the polymorphic lambda calculus based on the simple idea of a universe, is proposed. Although impossible in nonconstructive set theory, the notion is unproblematic for constructive sets, yields completeness and initiality theorems, and can be used to unify and relate many different notions of model that have been proposed in the literature, including those that extend the basic calculus with additional features such as fixpoints or a type of all types. Moreover, the polymorphic lambda calculus and Martin-Lof type theory are related by a map of logics. A categorical and initial model semantics is given for the basic calculus and for richer calculi that extend the basic one with fixpoints or with a type of all types.
Original language | English (US) |
---|---|
Title of host publication | Conf Rec Sixteenth Annu ACM Symp Princ Program Lang |
Publisher | Publ by ACM |
Pages | 228-241 |
Number of pages | 14 |
ISBN (Print) | 0897912942 |
State | Published - 1989 |
Externally published | Yes |
Event | Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages - Austin, TX, USA Duration: Jan 11 1989 → Jan 13 1989 |
Other
Other | Conference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages |
---|---|
City | Austin, TX, USA |
Period | 1/11/89 → 1/13/89 |
ASJC Scopus subject areas
- Engineering(all)