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.
|Title of host publication||Foundations of Software Science and Computation Structures|
|Subtitle of host publication||Proceedings of 7th International Conference, FOSSACS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 – April 2, 2004|
|Place of Publication||Berlin, Germany|
|Number of pages||15|
|Publication status||Published - 2004|
|Name||Lecture Notes in Computer Science|