Games and full abstraction for the lazy /spl lambda/-calculus
- 19 November 2002
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- Vol. 3 (10436871) , 234-243
- https://doi.org/10.1109/lics.1995.523259
Abstract
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.Keywords
This publication has 10 references indexed in Scilit:
- Functions as processesPublished by Springer Nature ,2005
- Equality in lazy computation systemsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- A fully abstract semantics for concurrent graph reductionPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Full Abstraction for PCF (extended abstract)Lecture Notes in Computer Science, 1994
- Lambda-Calculi for (Strict) Parallel FunctionsInformation and Computation, 1994
- Full Abstraction in the Lazy Lambda CalculusInformation and Computation, 1993
- Games and full Completeness for multiplicative Linear LogicLecture Notes in Computer Science, 1992
- Algebraically complete categoriesLecture Notes in Mathematics, 1991
- LCF considered as a programming languageTheoretical Computer Science, 1977
- Fully abstract models of typed λ-calculiTheoretical Computer Science, 1977