一句话：提出首个基于分离逻辑的 Hoare 式程序逻辑，用于推理良括号控制流，并在 Coq/Iris 中机械化。
良括号控制流要求被调用函数必须在调用者恢复执行前返回，这一性质在安全与正确性推理中很重要。已有工作主要在完全抽象博弈模型中将其刻画为策略条件，或使用复杂的关系模型与显式状态迁移系统来验证依赖良括号性的程序。本文提出首个基于分离逻辑的 Hoare 式程序逻辑，用于直接推理良括号控制流，并展示如何用该逻辑证明良括号程序的正确性；进一步基于该程序逻辑定义一元与二元逻辑关系模型。所有结果均在 Iris 框架之上形式化，并在 Coq 证明助手中机械化。
A program is said to be well-bracketed if every called function must return before its caller can resume execution. This is often the case. Well-bracketedness has been captured semantically as a condition on strategies in fully abstract games models and multiple prior works have studied well-bracketedness by showing correctness/security properties of programs where such properties depend on the well-bracketed nature of control flow. The latter category of prior works have all used involved relational models with explicit state-transition systems capturing the relevant parts of the control flow of the program. In this paper we present the first Hoare-style program logic based on separation logic for reasoning about well-bracketedness and use it to show correctness of well-bracketed programs both directly and also through defining unary and binary logical relations models based on this program logic. All results presented in this paper are formalized on top of the Iris framework and mechanized in the Coq proof assistant.
@article{paperbot2610,
title = {The Logical Essence of Well-Bracketed Control Flow},
author = {Amin Timany and Armaël Guéneau and Lars Birkedal},
journal = {Proceedings of the ACM on Programming Languages},
volume = {8},
number = {POPL},
year = {2024},
doi = {10.1145/3632862}
}