TY - CHAP
T1 - A game semantics of local names and good variables
AU - Laird, James
PY - 2004
Y1 - 2004
N2 - We describe a game semantics for local names in a functional setting. It is based on a category of dialogue games acted upon by the automorphism group of the natural numbers; this allows properties of names such as freshness and locality to be characterized semantically. We describe a model of the nu-calculus in this category, and extend it with named references (without bad variables) using names as pointers to a store. After refining the semantics via a notion of garbage collection, we prove that the compact elements are definable as terms, and hence obtain a full abstraction result.
AB - We describe a game semantics for local names in a functional setting. It is based on a category of dialogue games acted upon by the automorphism group of the natural numbers; this allows properties of names such as freshness and locality to be characterized semantically. We describe a model of the nu-calculus in this category, and extend it with named references (without bad variables) using names as pointers to a store. After refining the semantics via a notion of garbage collection, we prove that the compact elements are definable as terms, and hence obtain a full abstraction result.
UR - http://www.scopus.com/inward/record.url?scp=35048848009&partnerID=8YFLogxK
UR - http://dx.doi.org/10.1007/978-3-540-24727-2_21
U2 - 10.1007/978-3-540-24727-2_21
DO - 10.1007/978-3-540-24727-2_21
M3 - Book chapter
AN - SCOPUS:35048848009
SN - 9783540212980
T3 - Lecture Notes in Computer Science
SP - 289
EP - 303
BT - Foundations of Software Science and Computation Structures
A2 - Walukiewicz, I.
PB - Springer Verlag
CY - Berlin, Germany
ER -