paperbot · PL 论文追踪

全部论文 待读 收藏

P2 ReLoC

ReLoC：一种用于高阶状态、细粒度并发、多态与递归类型程序精化的逻辑
LICS Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science2018匹配度 3/10 · 论文属于形式化验证中的程序精化逻辑，与“用 LLM/Agent 改进形式化验证”仅存在间接关联，且完全不涉及 AI/LLM、静态分析、浮点程序分析或贝叶斯程序分析。引用 52 inbox
Dan Frumin, Robbert Krebbers, Lars Birkedal
程序验证形式语义
crossref: 2026-09-12

AI 速览

一句话：提出 ReLoC，一种用类型与结构导向规则证明高阶状态、细粒度并发、多态和递归类型程序精化的逻辑。

本文提出 ReLoC，一个用于证明具有高阶状态、细粒度并发、多态和递归类型的语言中程序精化（refinement）的逻辑。其核心判断 e ⪯ e' : τ 表示程序 e 在类型 τ 上精化程序 e'。与以往针对高阶状态和并发语言的精化工作不同，ReLoC 不是将判断展开为模型中的定义来进行证明，而是提供类型与结构导向的证明规则来操作该判断。这些更抽象的规则降低了精化证明的复杂度，使此类证明更容易开展。

问题
如何为含高阶状态、细粒度并发、多态和递归类型的语言提供便于使用的程序精化证明方法。
方法
定义一个核心精化判断 e ⪯ e' : τ，并为其设计类型与结构导向的证明规则，而非依赖展开模型定义。
评估
摘要未报告具体实现或案例评估；作者以更抽象证明规则使精化证明更简单来论证其价值。
原文摘要（Abstract）

We present ReLoC: a logic for proving refinements of programs in a language with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of our logic is a judgement e ⪯ e': τ, which expresses that a program e refines a program e' at type τ. In contrast to earlier work on refinements for languages with higher-order state and concurrency, ReLoC provides type- and structure-directed rules for manipulating this judgement, whereas previously, such proofs were carried out by unfolding the judgement into its definition in the model. These more abstract proof rules make it simpler to carry out refinement proofs.

链接与引用

DOI 原文 · PDF（开放获取） ·

BibTeX 
@inproceedings{paperbot4306,
  title = {ReLoC},
  author = {Dan Frumin and Robbert Krebbers and Lars Birkedal},
  booktitle = {LICS},
  year = {2018},
  doi = {10.1145/3209108.3209174}
}