论文标题
关于关系计划逻辑的单元的分歧
Divergences on Monads for Relational Program Logics
论文作者
论文摘要
已经引入了几种关系程序逻辑，以整合有关程序的关系性能的推理以及计算效应之间定量差异的测量。在本文中，我们将这种逻辑的一般框架形式化了计算效应之间的定量差异，因为差异是单元的分歧，然后开发了一个关系程序逻辑ACRL，该逻辑ACRL支持通用计算效应和对它们的分歧。为了提供ACRL支持差异的分类语义，我们提供了一种从单调上获得分级的强关系的方法。我们得出了ACRL的两个实例化，以验证1）高阶功能概率程序的各种差异隐私，以及2）具有概率选择和成本计数操作的高阶功能程序之间成本分布的差异。
Several relational program logics have been introduced for integrating reasoning about relational properties of programs and measurement of quantitative difference between computational effects. Towards a general framework for such logics, in this paper, we formalize quantitative difference between computational effects as divergence on monad, then develop a relational program logic acRL that supports generic computational effects and divergences on them. To give a categorical semantics of acRL supporting divergences, we give a method to obtain graded strong relational liftings from divergences on monads. We derive two instantiations of acRL for the verification of 1) various differential privacy of higher-order functional probabilistic programs and 2) difference of distribution of costs between higher-order functional programs with probabilistic choice and cost counting operations.
