我们引入一阶逻辑的一种扩展，它配备了用于对抽象状态进行推理的附加谓词。该逻辑中的矢列由一个主公式以及 Hoare 逻辑风格的预处理和后置条件组成，并且该逻辑的公理和规则确保关于状态的断言以正确的方式组合。本文的主要结果是我们逻辑的一个可实现性解释，它将程序提取到一种混合函数式/命令式语言中。所有可用这种语言表达的程序都以顺序方式作用于状态，我们通过在语义元理论中使用状态单子来解释它们，从而使这一直观认识变得精确。我们的基本框架非常通用，我们的意图是它可以以多种不同方式被实例化和扩展。我们详细概述了一个这样的扩展：带良基 while 规则的 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.
Fuzzi: A Three-Level Logic for Differential Privacy
敏感数据集的管理者有时需要知道对数据的查询是否是差异私有的[Dwork et al. 2006]。已经提出了两种逻辑来检查此属性：（1）类型系统和其他静态分析，它们完全自动化了诸如“程序敏感性”和“隐私丢失”等概念的直接推理，以及（2）成熟的程序逻辑，如apRHL（近似的、概率的、关系的霍尔逻辑）[Barthe等人，2016]，其支持关于微妙的隐私保护算法技术的更灵活的推理，但仅提供最小的自动化。我们提出了一个三层逻辑差分隐私在一个强制性的设置，并提出了一个原型实现Fuzzi。Fuzzi的最低层是通用逻辑;它的中间层是apRHL;它的顶层是一种新的灵敏度逻辑，它改编自Fuzz的线性逻辑启发类型系统，一种差分私有函数语言[Reed和Pierce 2010]。关键的新颖性在于灵敏度逻辑和两个较低层次逻辑之间的高度集成：灵敏度逻辑的判断和证明可以很容易地转化为apRHL;相反，关键算法构建块的隐私属性可以在apRHL和基本逻辑中手动证明，然后打包成类型规则，该类型规则可以由敏感性逻辑的检查器应用，以自动构造任意大小的复合程序的隐私证明。我们通过实现四种不同的私人机器学习算法来证明Fuzzi的实用性，并表明Fuzzi的检查器能够获得严格的灵敏度界限。
