Aarhus University Seal / Aarhus Universitets segl

Realisability semantics of parametric polymorphism, general references and recursive types

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

  • Lars Birkedal
  • Kristian Støvring, IT University of Copenhagen, Denmark
  • Jacob Thamsborg, IT University of Copenhagen, Denmark

We present a realisability 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 that include general reference types. The interpretation uses a new approach to modelling 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.

Original languageEnglish
JournalMathematical Structures in Computer Science
Pages (from-to)655-703
Number of pages49
Publication statusPublished - 1 Aug 2010
Externally publishedYes

See relations at Aarhus University Citationformats

ID: 81784212