Logical Relations and Parametricity - A Reynolds Programme for Category Theory and Programming Languages
Electronic Notes in Theoretical Computer Science(2014)
摘要
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.
更多查看译文
关键词
john reynolds,reynolds programme,programming languages,logical relations,seminal paper,category theory,higher-order type,parametric polymorphism,representation independence,renewed attempt,information hiding,mathematical theory,homomorphisms,universal algebra
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要