A Nominal Relational Model for Local Store

The theory of nominal sets is a theory for names, freshness and binders. It has recently been suggested as a framework for modelling local store because it allows for a more elementary development than the traditional presheaf models. However, when modelling the important principle of relational reasoning for local store all these models use families of relations indexed by relations on store, and thus essentially return to presheaf models on the relational level. In this paper we show how relational reasoning can also be modelled using nominal sets. Building on a model suggested by Pitts and Shinwell we construct a relational model for local store in nominal sets in which types are interpreted as relations. These relational interpretations of types capture, in a single relation for each type, the relational reasoning principle for local store which in previous models was captured using a family of relations for each type. The relational model also demonstrates how the relations constitute a model in their own right, which hopefully means that they can be used to construct better models. Using the relational model we construct a relational parametricity principle for the operation allocating local store, and we show how this implies the relational reasoning principle