Logical relations and parametricity - A Reynolds Programme for category theory and programming languages dedicated to the memory of John C. Reynolds, 1935-2013: in Proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013)

Claudio Hermida, Uday S. Reddy, Edmund P. Robinson

    Research output: Contribution to journalArticlepeer-review

    9 Citations (Scopus)

    Abstract

    In his seminal paper on "Types, Abstraction and Parametric Polymorphism," John Reynolds called for homomorphisms to be generalized from functions to relations. He reasoned that such a generalization would allow type-based "abstraction" (representation independence, information hiding, naturality or parametricity) to be captured in a mathematical theory, while accounting for higher-order types. However, after 30 years of research, we do not yet know fully how to do such a generalization. In this article, we explain the problems in doing so, summarize the work carried out so far, and call for a renewed attempt at addressing the problem.

    Original languageEnglish
    Pages (from-to)149-180
    Number of pages32
    JournalElectronic Notes in Theoretical Computer Science
    Volume303
    DOIs
    Publication statusPublished - 28 Mar 2014
    EventProceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013) - Bath, United Kingdom
    Duration: 1 Mar 20131 Mar 2013

    Keywords

    • Category Theory
    • Data abstraction
    • Definability
    • Fibrations
    • Homomorphisms
    • Information hiding
    • Logical Relations
    • Natural Transformations
    • Parametric polymorphism
    • Reflexive Graphs
    • Relation lifting
    • Relational Parametricity
    • Universal algebra

    ASJC Scopus subject areas

    • Theoretical Computer Science
    • Computer Science(all)

    Fingerprint

    Dive into the research topics of 'Logical relations and parametricity - A Reynolds Programme for category theory and programming languages dedicated to the memory of John C. Reynolds, 1935-2013: in Proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013)'. Together they form a unique fingerprint.

    Cite this