Paper: The Finitary Projection Model for Second Order Lambda Calculus and Solutions to Higher Order Domain Equations (at LICS 1986)

Authors: Roberto M. Amadio Kim B. Bruce Giuseppe Longo

Abstract

The second order lambda calculus is an extension of the typed lambda calculus which supports polymorphism by allowing abstraction over type variables. In this paper a new class of models for the second order lambda calculus is constructed using projections as type representatives in untyped models of the lambda calculus. It is shown how to use these models to solve high-order recursive domain equations. Finally a rich theory of second order lambda models over type-free structures is presented which relates types and terms, leading to a characterization of all equations between type expressions which hold in any of these models.

BibTeX

  @InProceedings{AmadioBruceLongo-TheFinitaryProjecti,
    author = 	 {Roberto M. Amadio and Kim B. Bruce and Giuseppe Longo},
    title = 	 {The Finitary Projection Model for Second Order Lambda Calculus and Solutions to Higher Order Domain Equations},
    booktitle =  {Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (LICS 1986)},
    year =	 {1986},
    month =	 {June}, 
    pages =      {122--130},
    location =   {Cambridge, MA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }