Full abstraction for nominal general references

TL;DR

This paper develops a fully abstract game semantics for a language with nominal general references, extending the application of game semantics to stateful, name-based computational effects.

Contribution

It introduces a novel fully abstract semantics for languages with nominal general references using nominal games, advancing the theoretical understanding of stateful name-based effects.

Findings

Successfully models nominal general references in game semantics

Achieves full abstraction for the language with nominal references

Extends the scope of game semantics to stateful, name-based effects

Abstract

Game semantics has been used with considerable success in formulating fully abstract semantics for languages with higher-order procedures and a wide range of computational effects. Recently, nominal games have been proposed for modelling functional languages with names. These are ordinary, stateful games cast in the theory of nominal sets developed by Pitts and Gabbay. Here we take nominal games one step further, by developing a fully abstract semantics for a language with nominal general references.