一句话：提出带抽象 Hoare 三元组的一阶逻辑，并用可实现性解释将证明抽取为有状态程序。
论文扩展一阶逻辑，引入用于推理抽象状态的额外谓词，并将 sequent 表示为带有 Hoare 风格前置/后置条件的主公式；公理与规则保证状态断言正确组合。核心贡献是对该逻辑给出可实现性解释，将证明抽取为混合函数式/命令式语言中的程序。该语言中的程序以顺序方式作用于状态，作者用 state monad 在语义元理论中精确刻画这一直觉。框架具有一般性，可实例化与扩展；文中详细展示带良基 while 规则的 monadic Heyting 算术作为扩展，并讨论未来方向。
We introduce an extension of first-order logic that comes equipped with additional predicates for reasoning about an abstract state. Sequents in the logic comprise a main formula together with pre- and postconditions in the style of Hoare logic, and the axioms and rules of the logic ensure that the assertions about the state compose in the correct way. The main result of the paper is a realizability interpretation of our logic that extracts programs into a mixed functional/imperative language. All programs expressible in this language act on the state in a sequential manner, and we make this intuition precise by interpreting them in a semantic metatheory using the state monad. Our basic framework is very general, and our intention is that it can be instantiated and extended in a variety of different ways. We outline in detail one such extension: A monadic version of Heyting arithmetic with a wellfounded while rule, and conclude by outlining several other directions for future work.
@article{paperbot2784,
title = {Proofs as stateful programs: A first-order logic with abstract Hoare triples, and an interpretation into an imperative language},
author = {Thomas Powell},
journal = {Logical Methods in Computer Science},
volume = {Volume 20, Issue 1},
year = {2024},
doi = {10.46298/lmcs-20(1:7)2024}
}