Realisability semantics of parametric polymorphism, general references and recursive types

Lars Birkedal, Kristian Støvring, Jacob Junker Thamsborg

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

    Abstract

    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.
    OriginalsprogEngelsk
    TidsskriftMathematical Structures in Computer Science
    Vol/bind20
    Udgave nummer4
    Sider (fra-til)655-703
    ISSN0960-1295
    StatusUdgivet - 2010

    Emneord

    • Realizability model
    • Parametric polymorphism
    • First-class references
    • Recursive types
    • Kripke logical relations

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'Realisability semantics of parametric polymorphism, general references and recursive types'. Sammen danner de et unikt fingeraftryk.

    Citationsformater