Logic in Computer Science (LICS 1988)

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 Symp. on Logic in Computer Science, {LICS} 1988},
    year =	 1988,
    editor =	 {Yuri Gurevich},
    month =	 {July}, 
    pages =      {274--279},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }