A game semantics of names and pointers

Citations of this article
Mendeley users who have this article in their library.


We describe a fully abstract semantics for a simple functional language with locally declared names which may be used as pointers to names. It is based on a category of dialogue games acted upon by the group of natural number automorphisms. This allows a formal, semantic characterization of the key properties of names such as freshness and locality. We describe a model of the call-by-value λ-calculus (a closed Freyd category) based on these games, and show that it can be used to interpret the nu-calculus of Pitts and Stark. We then construct a model of our pointer-language by extending our category of games with an explicit representation of the store, using a notion of semantic garbage-collection to erase inaccessible pointers. Using factorization and decomposition techniques, we show that the compact elements of our model are definable as terms, and hence it is fully abstract. © 2007 Elsevier B.V. All rights reserved.




Laird, J. (2008). A game semantics of names and pointers. Annals of Pure and Applied Logic, 151(2–3), 151–169. https://doi.org/10.1016/j.apal.2007.10.006

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free