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

doi:10.1016/j.entcs.2014.02.008

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

The University of Birmingham

Research output: Contribution to journal › Article › peer-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 language	English
Pages (from-to)	149-180
Number of pages	32
Journal	Electronic Notes in Theoretical Computer Science
Volume	303
DOIs	https://doi.org/10.1016/j.entcs.2014.02.008
Publication status	Published - 28 Mar 2014
Event	Proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013) - Bath, United Kingdom Duration: 1 Mar 2013 → 1 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
General Computer Science

Access to Document

10.1016/j.entcs.2014.02.008

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

Hermida, C., Reddy, U. S., & Robinson, E. P. (2014). 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). Electronic Notes in Theoretical Computer Science, 303, 149-180. https://doi.org/10.1016/j.entcs.2014.02.008

Hermida, Claudio ; Reddy, Uday S. ; Robinson, Edmund P. / 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). In: Electronic Notes in Theoretical Computer Science. 2014 ; Vol. 303. pp. 149-180.

@article{d216e5574f2a4f5d8f4855f8cd27e909,

title = "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)",

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.",

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

author = "Claudio Hermida and Reddy, {Uday S.} and Robinson, {Edmund P.}",

year = "2014",

month = mar,

day = "28",

doi = "10.1016/j.entcs.2014.02.008",

language = "English",

volume = "303",

pages = "149--180",

journal = "Electronic Notes in Theoretical Computer Science",

issn = "1571-0661",

publisher = "Elsevier",

note = "Proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013) ; Conference date: 01-03-2013 Through 01-03-2013",

}

Hermida, C, Reddy, US & Robinson, EP 2014, '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)', Electronic Notes in Theoretical Computer Science, vol. 303, pp. 149-180. https://doi.org/10.1016/j.entcs.2014.02.008

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). / Hermida, Claudio; Reddy, Uday S.; Robinson, Edmund P.
In: Electronic Notes in Theoretical Computer Science, Vol. 303, 28.03.2014, p. 149-180.

Research output: Contribution to journal › Article › peer-review

TY - JOUR

T1 - Logical relations and parametricity - A Reynolds Programme for category theory and programming languages dedicated to the memory of John C. Reynolds, 1935-2013

T2 - Proceedings of the Workshop on Algebra, Coalgebra and Topology (WACT 2013)

AU - Hermida, Claudio

AU - Reddy, Uday S.

AU - Robinson, Edmund P.

PY - 2014/3/28

Y1 - 2014/3/28

N2 - 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.

AB - 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.

KW - Category Theory

KW - Data abstraction

KW - Definability

KW - Fibrations

KW - Homomorphisms

KW - Information hiding

KW - Logical Relations

KW - Natural Transformations

KW - Parametric polymorphism

KW - Reflexive Graphs

KW - Relation lifting

KW - Relational Parametricity

KW - Universal algebra

UR - http://www.scopus.com/inward/record.url?scp=84896486249&partnerID=8YFLogxK

U2 - 10.1016/j.entcs.2014.02.008

DO - 10.1016/j.entcs.2014.02.008

M3 - Article

AN - SCOPUS:84896486249

SN - 1571-0661

VL - 303

SP - 149

EP - 180

JO - Electronic Notes in Theoretical Computer Science

JF - Electronic Notes in Theoretical Computer Science

Y2 - 1 March 2013 through 1 March 2013

ER -

Hermida C, Reddy US, Robinson EP. 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). Electronic Notes in Theoretical Computer Science. 2014 Mar 28;303:149-180. doi: 10.1016/j.entcs.2014.02.008