一句话：提出 ReLoC 新版本，为高阶状态与细粒度并发程序提供机械化关系分离逻辑，支持精化证明与逻辑原子关系规约。
ReLoC 是证明程序精化的关系分离逻辑，面向高阶状态、细粒度并发、多态和递归类型。此前工作常需将精化判断展开到语义模型中，证明繁琐。本文提出 ReLoC 新版本：核心判断为 e ⪯ e' : τ，提供类型导向结构规则和分离逻辑风格符号执行规则，使精化证明更易进行，并把逻辑原子规约推广为逻辑原子关系规约。作者基于 Iris 在 Coq 中构建 ReLoC，证明可靠性并实现交互证明 tactic。ReLoC Reloaded 扩展 ReLoC (LICS'18)，加入新 Coq 机械化、Iris prophecy variables 支持，以及基于 HOCAP 模式的逻辑原子关系规约，并在 Coq 中机械化若干案例研究。
We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of ReLoC is its refinement judgment $e \precsim e' : \tau$, which states that a program $e$ refines a program $e'$ at type $\tau$. ReLoC provides type-directed structural rules and symbolic execution rules in separation-logic style for manipulating the judgment, whereas in prior work on refinements for languages with higher-order state and concurrency, such proofs were carried out by unfolding the judgment into its definition in the model. ReLoC's abstract proof rules make it simpler to carry out refinement proofs, and enable us to generalize the notion of logically atomic specifications to the relational case, which we call logically atomic relational specifications. We build ReLoC on top of the Iris framework for separation logic in Coq, allowing us to leverage features of Iris to prove soundness of ReLoC, and to carry out refinement proofs in ReLoC. We implement tactics for interactive proofs in ReLoC, allowing us to mechanize several case studies in Coq, and thereby demonstrate the practicality of ReLoC. ReLoC Reloaded extends ReLoC (LICS'18) with various technical improvements, a new Coq mechanization, and support for Iris's prophecy variables. The latter allows us to carry out refinement proofs that involve reasoning about the program's future. We also expand ReLoC's notion of logically atomic relational specifications with a new flavor based on the HOCAP pattern by Svendsen et al.
@article{paperbot1298,
title = {ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity},
author = {Dan Frumin and Robbert Krebbers and Lars Birkedal},
journal = {Logical Methods in Computer Science},
volume = {Volume 17, Issue 3},
year = {2021},
doi = {10.46298/lmcs-17(3:9)2021}
}