A Relational Logic for Higher-Order Programs
A Relational Logic for Higher-Order Programs
复制标题
DOI：
10.1145/3110265
复制
发表时间：
2017-09-01
影响因子：
1.8
通讯作者：
Strub, Pierre-Yves
中科院分区：
文献类型：
--
作者：
Aguirre, Alejandro;Barthe, Gilles;Strub, Pierre-Yves
关系程序验证是程序验证的一种变体，其中可以对两个程序进行推理，作为一种特殊情况，可以关于单个程序在不同输入上的两次执行。关系程序验证可用于对广泛的属性进行推理，包括等价性和精化，以及诸如连续性、信息流安全或相对成本等专门概念。在更高级别的设置中，可以使用关系精化类型系统来实现关系程序验证，关系精化类型系统是一种精化类型，其中断言具有关系解释。关系求精类型系统擅长关联结构等价的项，但对具有不同结构的项的关联支持有限.我们提出了一种称为关系高阶逻辑(RHOL)的逻辑，用于证明具有归纳类型和递归定义的简单类型Lambda演算的关系性质.RHOL保留了关系精化类型系统的类型导向风格，但通过同时对这两个术语进行推理的规则以及只考虑这两个术语之一的规则实现了更强的表现力。通过证明RHOL与高阶逻辑(HOL)的等价性，我们证明了RHOL具有很强的基础，并利用这种等价性导出了关键的元理论性质：主题约简、传递性规则的可容许性和集合论的可靠性。此外，我们为几个现有的关系类型系统定义了合理的嵌入，例如关系求精类型和用于依赖分析和相对代价的类型系统，并验证了以前工作无法达到的例子。
Relational program verification is a variant of program verification where one can reason about two programs and as a special case about two executions of a single program on different inputs. Relational program verification can be used for reasoning about a broad range of properties, including equivalence and refinement, and specialized notions such as continuity, information flow security or relative cost. In a higher-order setting, relational program verification can be achieved using relational refinement type systems, a form of refinement types where assertions have a relational interpretation. Relational refinement type systems excel at relating structurally equivalent terms but provide limited support for relating terms with very different structures.We present a logic, called Relational Higher Order Logic (RHOL), for proving relational properties of a simply typed lambda-calculus with inductive types and recursive definitions. RHOL retains the type-directed flavour of relational refinement type systems but achieves greater expressivity through rules which simultaneously reason about the two terms as well as rules which only contemplate one of the two terms. We show that RHOL has strong foundations, by proving an equivalence with higher-order logic (HOL), and leverage this equivalence to derive key meta-theoretical properties: subject reduction, admissibility of a transitivity rule and set-theoretical soundness. Moreover, we define sound embeddings for several existing relational type systems such as relational refinement types and type systems for dependency analysis and relative cost, and we verify examples that were out of reach of prior work.