TY - JOUR
T1 - A game semantics of names and pointers
AU - Laird, J.
PY - 2008/2
Y1 - 2008/2
N2 - 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.
AB - 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.
KW - Fresh name generation
KW - Game semantics
KW - Pointer-based storage
UR - http://www.scopus.com/inward/record.url?scp=38649099744&partnerID=8YFLogxK
UR - http://dx.doi.org/10.1016/j.apal.2007.10.006
UR - http://dx.doi.org/10.1016/j.apal.2007.10.006
U2 - 10.1016/j.apal.2007.10.006
DO - 10.1016/j.apal.2007.10.006
M3 - Article
AN - SCOPUS:38649099744
SN - 0168-0072
VL - 151
SP - 151
EP - 169
JO - Annals of Pure and Applied Logic
JF - Annals of Pure and Applied Logic
IS - 2-3
ER -