面向连续随机采样的近似关系霍尔逻辑
计算机科学中的逻辑
2016-12-20 v1
摘要
近似关系霍尔逻辑（apRHL）是一种用于形式化验证以编程语言 pWHILE 编写的数据库差分隐私的逻辑。然而，严格来说，该逻辑仅处理离散随机采样。在本文中，我们定义了描述差分隐私的 Giry 单子的次概率变体的分级关系提升。我们利用这种分级提升扩展了逻辑 apRHL，以处理连续随机采样。我们给出了一种为连续随机采样提供 apRHL 证明规则的通用方法。
引用
@article{arxiv.1603.01445,
title = {Approximate Relational Hoare Logic for Continuous Random Samplings},
author = {Tetsuya Sato},
journal= {arXiv preprint arXiv:1603.01445},
year = {2016}
}