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.

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