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 Symp. on Logic in Computer Science, {LICS} 1993},
    year =	 1993,
    editor =	 {Moshe Vardi},
    month =	 {June}, 
    pages =      {6--14},
    location =   {Montreal, Canada}, 
    publisher =	 {IEEE Computer Society Press}
  }