ReLoC Reloaded：面向细粒度并发与逻辑原子性的机械化关系逻辑
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
AI总结：
本文提出ReLoC Reloaded，一种基于Iris框架的机械化关系分离逻辑，用于证明高阶状态与细粒度并发程序的精化关系，并扩展了逻辑原子关系规范，支持预言变量以增强实用性。
摘要：
我们提出了一个新版本的ReLoC：一种关系分离逻辑，用于证明具有高阶状态、细粒度并发、多态性和递归类型的程序之间的精化关系。ReLoC的核心是其精化判断 $e \precsim e' : τ$，它表示程序 $e$ 在类型 $τ$ 下精化程序 $e'$。ReLoC提供了类型导向的结构规则和分离逻辑风格的符号执行规则来操作该判断，而在先前关于具有高阶状态和并发的语言精化的研究中，此类证明是通过将判断展开为其在模型中的定义来进行的。ReLoC的抽象证明规则使得进行精化证明更加简单，并使我们能够将逻辑原子规范的概念推广到关系情形，我们称之为逻辑原子关系规范。\n 我们在Coq中的Iris框架基础上构建ReLoC，从而能够利用Iris的特性来证明ReLoC的可靠性，并在ReLoC中进行精化证明。我们实现了用于ReLoC中交互式证明的策略，使我们能够在Coq中机械化多个案例研究，从而展示ReLoC的实用性。\n ReLoC Reloaded在ReLoC（LICS'18）的基础上进行了多项技术改进，提供了新的Coq机械化实现，并支持Iris的预言变量。后者使我们能够进行涉及程序未来推理的精化证明。我们还扩展了ReLoC的逻辑原子关系规范概念，新增了一种基于Svendsen等人提出的HOCAP模式的新风格。
英文摘要：
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' : τ$, which states that a program $e$ refines a program $e'$ at type $τ$. 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
