Lics

IEEE Symposium on Logic in Computer Science

LICS Home - LICS Awards - LICS Newsletters - LICS Archive - LICS Organization - Logic-Related Conferences - Links

Eighth Annual IEEE Symposium on

Logic in Computer Science (LICS 1993)

Paper: The genericity theorem and the notion of parametricity in the polymorphic λ-calculus (at LICS 1993)

Authors: Giuseppe Longo Kathleen Milsted Sergei Soloviev

Abstract

The authors focus on how polymorphic functions, which may take types as inputs, depend on types. These functions are generally understood to have an essentially constant meaning, in all models, on input types. It is shown how the proof theory of the polymorphic λ-calculus suggests a clear syntactic description of this phenomenon. Under a reasonable condition, it is shown that identity of two polymorphic functions on a single type implies identity of the functions (equivalently, every type is a generic input)

BibTeX

  @InProceedings{LongoMilstedSolovie-Thegenericitytheore,
    author = 	 {Giuseppe Longo and Kathleen Milsted and Sergei Soloviev},
    title = 	 {The genericity theorem and the notion of parametricity in the polymorphic λ-calculus },
    booktitle =  {Proceedings of the Eighth Annual IEEE Symposium on Logic in Computer Science (LICS 1993)},
    year =	 {1993},
    month =	 {June}, 
    pages =      {6--14},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }
   

Last modified: 2018-06-2121:59
Andrzej Murawski