A game semantics of names and pointers

Research output: Contribution to journalArticlepeer-review

16 Citations (SciVal)

Abstract

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.

Original languageEnglish
Pages (from-to)151-169
Number of pages19
JournalAnnals of Pure and Applied Logic
Volume151
Issue number2-3
DOIs
Publication statusPublished - Feb 2008

Keywords

  • Fresh name generation
  • Game semantics
  • Pointer-based storage

Fingerprint

Dive into the research topics of 'A game semantics of names and pointers'. Together they form a unique fingerprint.

Cite this