Title :
Games and full abstraction for the lazy λ-calculus
Author :
Abramsky, Samson ; McCusker, Guy
Author_Institution :
Dept. of Comput., Imperial Coll. of Sci., Technol. & Med., London, UK
Abstract :
We define a category of games 𝒢, and its extensional quotient ℰ. A model of the lazy X-calculus, a type-free functional language based on evaluation to weak head normal form, is given in 𝒢, yielding an extensional model in ℰ. 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
Keywords :
formal languages; game theory; lambda calculus; programming languages; extensional model; extensional quotient; full abstraction; fully abstract model; games; lazy X-calculus; lazy lambda-calculus; purely semantic construction; reflexively-typed sequential language; type-free functional language; weak head normal form; Calculus; Computational modeling; Educational institutions; Game theory; Head;
Conference_Titel :
Logic in Computer Science, 1995. LICS '95. Proceedings., Tenth Annual IEEE Symposium on
Conference_Location :
San Diego, CA
Print_ISBN :
0-8186-7050-9
DOI :
10.1109/LICS.1995.523259
