Realizability Semantics of Parametric Polymorphism, General References, and Recursive Types

The authors present a realizability model for a call-by-value, higher-order programming language with parametric polymorphism, general first-class references, and recursive types. The main novelty is a relational interpretation of open types (as needed for parametricity reasoning) that include general reference types. The interpretation uses a new approach to modeling references. The universe of semantic types consists of world-indexed families of logical relations over a universal pre-domain. In order to model general reference types, worlds are nite maps from locations to semantic types: this introduces a circularity between semantic types and worlds that precludes a direct definition of either.