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 key properties of names such as freshness and locality.

We describe a model of the call-by-value lambda-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.

  • Full text (.pdf)
  • Extended abstract (.pdf) (presented at FoSSaCS '04).
  • Slides (.pdf) from the conference presentation.
  • Bibtex entry
    @article{apal08,
    author = "J. Laird",
    title = "A Game Semantics of Names and Pointers",
    journal = "Annals of Pure and Applied Logic",
    issue = 2,
    pages = "151--169",
    volume =151,
    year = 2008}