paperbot · PL 论文追踪

全部论文 待读 收藏

P2 A General Framework for Relational Parametricity

关系参数性的一个通用框架
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 2/10 · 论文属于纯类型论/形式语义方向,讨论关系参数性的元理论基础,不涉及静态分析、LLM/Agent、浮点程序分析或贝叶斯程序分析等用户核心方向。虽然属于 PL 领域,但与其研究画像中的交叉点几乎无直接关联。引用 0 inbox
Kristina Sojakova, Patricia Johann
crossref: 2026-09-12

AI 速览

一句话:提出了一个能忠实表达 Reynolds 原始关系参数性理论的一般框架。

Reynolds 最初的关系参数性理论旨在刻画多态 System F 程序保持输入之间所有关系这一现象。但他后来表明,该理论只能在具有非直谓宇宙的元理论中表述,例如归纳构造演算。此后出现了若干更抽象的关系参数性处理方式;本文表明,这些处理似乎都无法令人满意地表达 Reynolds 的原始理论。为此,本文提出一个通用框架来刻画关系参数性,并据此分析既有抽象方法的局限,目标是在合适的元理论中忠实复现 Reynolds 原始理论的核心思想。

问题
Reynolds 的关系参数性理论只能在不具有直谓限制的元理论中表述,而现有更抽象的处理方式均未能令人满意地表达其原始理论。
方法
提出一个关系参数性的通用框架,并用它来分析和比较已有抽象处理与 Reynolds 原始理论之间的关系。
评估
通过理论层面的比较与论证,说明既有抽象处理无法令人满意地表达 Reynolds 原始关系参数性理论。
原文摘要(Abstract)

Reynolds' original theory of relational parametricity was intended to capture the observation that polymorphically typed System F programs preserve all relations between inputs. But as Reynolds himself later showed, his theory can only be formulated in a metatheory with an impredicative universe, such as the Calculus of Inductive Constructions. A number of more abstract treatments of relational parametricity have since appeared; however, as we show, none of these seem to express Reynolds' original theory in a satisfactory way.

链接与引用

DOI 原文 · PDF(开放获取) ·

BibTeX
@inproceedings{paperbot4335,
  title = {A General Framework for Relational Parametricity},
  author = {Kristina Sojakova and Patricia Johann},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209141}
}