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)

Research output: Contribution to journalArticle

Authors

External organisations

  • Queen Mary University of London

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.

Details

Original languageEnglish
Pages (from-to)149-180
Number of pages32
JournalElectronic Notes in Theoretical Computer Science
Volume303
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