Games and full abstraction for the lazy λ-calculus
Samson Abramsky, Guy McCusker · 2002
We define a category of games /spl Gscr/, and its extensional quotient /spl Escr/. A model of the lazy X-calculus, a type-free functional language based on evaluation to weak head normal form, is given in /spl Gscr/, yielding an extensional model in /spl Escr/. This model is shown to be fully abstract with respect to applicative simulation. This is, so fear as we known, the first purely semantic construction of a fully abstract model for a reflexively-typed sequential language.