一句话：提出 LHC 逻辑，以超三元组作为统一组合构件，实现更强的 hypersafety 证明组合性。
高阶安全性（hypersafety）性质刻画一个程序或一组程序的多条执行迹之间的关系，如确定性、幂等性与结合性。已有关系程序逻辑利用被关联程序的结构相似性来简化证明，但组合性受限。本文提出一种新的互补证明原则，将“超三元组”（hyper-triple）作为统一的组合式证明构件，并据此设计超三元组组合逻辑 LHC。LHC 支持以往逻辑难以实现的证明组合方式；作者证明其可靠性，并在若干有挑战性的例子中应用，展示其表达能力与实用性。
Hypersafety properties of arity n are program properties that relate n traces of a program (or, more generally, traces of n programs). Classic examples include determinism, idempotence, and associativity. A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler proofs by capitalizing on structural similarities between the n related programs. We propose an unexplored, complementary proof principle that establishes hyper-triples (i.e. hypersafety judgments) as a unifying compositional building block for proofs, and we use it to develop a Logic for Hyper-triple Composition (LHC), which supports forms of proof compositionality that were not achievable in previous logics. We prove LHC sound and apply it to a number of challenging examples.
@article{paperbot1461,
title = {Proving hypersafety compositionally},
author = {Emanuele D’Osualdo and Azadeh Farzan and Derek Dreyer},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563298}
}