Paper: Games and Full Abstraction for the Lazy Lambda-Calculus (at LICS 1995)

Authors: Samson Abramsky Guy McCusker

Abstract

We define a category of games G, and its extensional quotient E. A model of the lazy lambda-calculus, a type-free functional language based on evaluation to weak head normal form, is given in G, yielding an extensional model in E. This model is shown to be fully abstract with respect to applicative simulation. This is, so far as we know, the first purely semantic construction of a fully abstract model for a reflexively-typed sequential language.

BibTeX

  @InProceedings{AbramskyMcCusker-GamesandFullAbstrac,
    author = 	 {Samson Abramsky and Guy McCusker},
    title = 	 {Games and Full Abstraction for the Lazy Lambda-Calculus},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symposium on Logic in Computer Science (LICS 1995)},
    year =	 {1995},
    month =	 {June}, 
    pages =      {234--243},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}
  }