Categorical Models of Abadi-Plotkin's logic for parametricity

    Publikation: Artikel i tidsskrift og konference artikel i tidsskriftTidsskriftartikelForskningpeer review

    Abstract

    We propose a new category-theoretic formulation of relational parametricity based on a logic for reasoning about parametricity given by Abadi and Plotkin (Plotkin and Abadi, 1993). The logic can be used to reason about parametric models, such that we may prove consequences of parametricity that to our knowledge have not been proved before for
    existing category-theoretic notions of relational parametricity. We provide examples of parametric models and we describe a way of constructing parametric models from given models of the second-order lambda calculus.
    OriginalsprogEngelsk
    TidsskriftMathematical Structures in Computer Science
    Vol/bind15
    Udgave nummer4
    Sider (fra-til)709-772
    Antal sider64
    ISSN0960-1295
    StatusUdgivet - 2005

    Emneord

    • Abadi-Plotkin logic
    • Categorical models
    • Parametricity
    • Theoretical computer science

    Fingeraftryk

    Dyk ned i forskningsemnerne om 'Categorical Models of Abadi-Plotkin's logic for parametricity'. Sammen danner de et unikt fingeraftryk.

    Citationsformater