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.

翻译：我们提出一种扩展的一阶逻辑，该逻辑配备了用于推理抽象状态的附加谓词。该逻辑中的相继式包含一个主公式以及霍尔逻辑风格的前置条件和后置条件，逻辑的公理和规则确保关于状态的断言以正确方式组合。本文的主要结果是该逻辑的可实现性解释，它将程序提取为混合函数式/命令式语言。该语言中所有可表达的程序都以顺序方式作用于状态，我们通过使用状态单子在语义元理论中对其进行解释，使这一直觉精确化。我们的基础框架具有高度通用性，并旨在以多种不同方式实例化和扩展。我们详细概述了一种扩展：带良基while规则的Heyting算术的单子版本，最后概述了未来工作的其他方向。