Logic in Computer Science (LICS 1990)

Paper: A PER model of polymorphism and recursive types (at LICS 1990)

Authors: Abadi, M. Plotkin, G.D.

Abstract

A model of Reynold's polymorphic lambda calculus is provided, which also allows the recursive definition of elements and types. The techniques uses a good class of partial equivalence relations (PERs) over a certain CPO. This allows the combination of inverse-limits for recursion and intersection for polymorphism

BibTeX

  @InProceedings{AbadiPlotkin-APERmodelofpolymorp,
    author = 	 {Abadi, M. and Plotkin, G.D.},
    title = 	 {A PER model of polymorphism and recursive types},
    booktitle =  {Proceedings of the Fifth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1990},
    year =	 1990,
    editor =	 {John Mitchell},
    month =	 {June}, 
    pages =      {355--365},
    location =   {Philadelphia, PA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }