Paper: Semantic parametricity in polymorphic lambda calculus (at LICS 1988)

Authors: Peter J. Freyd Jean-Yves Girard Andre Scedrov Philip J. Scott

Abstract

A semantic condition necessary for the parametricity of polymorphic functions is considered. One of its instances is the stability condition for elements of variable type in the coherent domains semantics. A larger setting is presented that does not use retract pairs and keeps intact a basic feature of a certain function-type constructor. Polymorphic lambda terms are semantically parametric because of normalization

BibTeX

  @InProceedings{FreydGirardScedrovS-Semanticparametrici,
    author = 	 {Peter J. Freyd and Jean-Yves Girard and Andre Scedrov and Philip J. Scott},
    title = 	 {Semantic parametricity in polymorphic lambda calculus},
    booktitle =  {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)},
    year =	 {1988},
    month =	 {July}, 
    pages =      {274--279},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }