A Game Semantics of Local Names and Good Variables

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 full abstraction result.

• Type: Conference
• Year: 2004
• Where: FOSSACS
• Authors: James Laird
• Keywords: Applied Computing, FOSSACS 2004, Functional Setting, Game Semantics, Local Names