Relating models of polymorphism

Research output: Chapter in Book/Report/Conference proceedingConference contribution

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 languageEnglish (US)
Title of host publicationConf Rec Sixteenth Annu ACM Symp Princ Program Lang
PublisherPubl by ACM
Pages228-241
Number of pages14
ISBN (Print)0897912942
StatePublished - 1989
Externally publishedYes
EventConference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages - Austin, TX, USA
Duration: Jan 11 1989Jan 13 1989

Other

OtherConference Record of the Sixteenth Annual ACM Symposium on Principles of Programming Languages
CityAustin, TX, USA
Period1/11/891/13/89

ASJC Scopus subject areas

  • Engineering(all)

Fingerprint

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

Cite this