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 - Chapter or section

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 -