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.

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