TY - JOUR
T1 - Realisability semantics of parametric polymorphism, general references and recursive types
AU - Birkedal, Lars
AU - Støvring, Kristian
AU - Thamsborg, Jacob Junker
PY - 2010
Y1 - 2010
N2 - We present a realizability model for a call-by-value, higherorder 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 predomain. In order to model general reference types, worlds are finite maps from locations to semantic types: this introduces a circularity between semantic types and worlds that precludes a direct definition of either. Our solution is to solve a recursive equation in an appropriate category of metric spaces. In effect, types are interpreted using a Kripke logical relation over a recursively defined set of worlds. We illustrate how the model can be used to prove simple equivalences between different implementations of imperative abstract data types.
AB - We present a realizability model for a call-by-value, higherorder 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 predomain. In order to model general reference types, worlds are finite maps from locations to semantic types: this introduces a circularity between semantic types and worlds that precludes a direct definition of either. Our solution is to solve a recursive equation in an appropriate category of metric spaces. In effect, types are interpreted using a Kripke logical relation over a recursively defined set of worlds. We illustrate how the model can be used to prove simple equivalences between different implementations of imperative abstract data types.
KW - Realizability model
KW - Parametric polymorphism
KW - First-class references
KW - Recursive types
KW - Kripke logical relations
KW - Realizability model
KW - Parametric polymorphism
KW - First-class references
KW - Recursive types
KW - Kripke logical relations
M3 - Journal article
SN - 0960-1295
VL - 20
SP - 655
EP - 703
JO - Mathematical Structures in Computer Science
JF - Mathematical Structures in Computer Science
IS - 4
ER -