Paper: A fixed point of the second order lambda-calculus: observable equivalences and models (at LICS 1988)

Authors: Roberto M. Amadio

Abstract

The author develops an operational model of an impredicative version of explicit polymorphism, namely, an extension of the second-order lambda-calculus, including a fixed-point combinator and a multisorted first-order algebra. He shows that the typical properties of the λ-calculus are preserved, and he investigates novel aspects that arise from second-order type structure as well as the relationships with well-known, simply typed, PCF-like languages. A suitable theory of observably equivalent terms is defined, and its complexity is explored. A denotional model suggesting interesting extensions of a language is studied

BibTeX

  @InProceedings{Amadio-Afixedpointofthesec,
    author = 	 {Roberto M. Amadio},
    title = 	 {A fixed point of the second order lambda-calculus: observable equivalences and models },
    booktitle =  {Proceedings of the Third Annual IEEE Symposium on Logic in Computer Science (LICS 1988)},
    year =	 {1988},
    month =	 {July}, 
    pages =      {51--60},
    location =   {Edinburgh, Scotland, UK}, 
    publisher =	 {IEEE Computer Society Press}
  }