一句话：首次给出 Iris 程序逻辑完备性证明方法，并在 Rocq 中机器化验证多种逻辑。
程序逻辑通常需要可靠性与完备性两个核心定理：可靠性保证逻辑推导正确，完备性保证逻辑能表达所有正确结论。Iris 已成为构造分离逻辑的通用基础，但其衍生逻辑此前只有可靠性证明，缺乏完备性证明。本文提出首个建立 Iris 程序逻辑完备性的方法，并将其推广到多种已有逻辑：高阶 ML 式语言的部分与全并发分离逻辑、两种定量逻辑（执行时间界与概率错误界）以及用于证明精化的关系逻辑。所有结果均在 Rocq 证明助手中机器化验证。
Traditionally, proof systems such as program logics come with two core theorems: soundness and completeness . The role of soundness is obvious: we want to be sure that arguments carried out inside the logic actually lead to correct conclusions. Completeness complements that by ensuring that the logic does not limit expressivity: in principle, any correct result can be obtained within the confines of the logic. This result typically has to be stated relative to the completeness of the assertion logic that is used to reason about pre- and postconditions. Over the past decade, the Iris framework has emerged as a widely used foundation for building separation logics. While Iris-based logics typically come with a soundness proof, none of them have had a proof of completeness. In this paper, we present the first approach for establishing completeness of Iris-based program logics, and we show the generality of our methodology by applying it to a range of different logics described in prior work, including partial and total concurrent separation logics for a higher-order ML-like language, two quantitative logics (for bounding execution time and probabilistic errors), and a relational logic for proving refinement. All our results have been mechanized in the Rocq prover.
@article{HostertZLGJT26,
title = {Completeness of Iris-Based Program Logics},
author = {Johannes Hostert and Zichen Zhang and Puming Liu and Simon Oddershede Gregersen and Ralf Jung and Joseph Tassarotti},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828682}
}