Tenth Annual IEEE Symposium on

Logic in Computer Science (LICS 1995)

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

Authors: Samson Abramsky Guy McCusker


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.


    author = 	 {Samson Abramsky and Guy McCusker},
    title = 	 {Games and Full Abstraction for the Lazy Lambda-Calculus},
    booktitle =  {Proceedings of the Tenth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1995},
    year =	 1995,
    editor =	 {Dexter Kozen},
    month =	 {June}, 
    pages =      {234-243},
    location =   {San Diego, CA, USA}, 
    publisher =	 {IEEE Computer Society Press}