Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
Probabilistic Functions and Cryptographic Oracles in Higher Order Logic
复制标题
高阶逻辑中的概率函数和密码预言
DOI：
10.1007/978-3-662-49498-1_20
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
A. Lochbihler
中科院分区：
文献类型：
--
作者：
A. Lochbihler
本文提出了一种概率函数程序设计语言在高阶逻辑中的浅嵌入。该语言具有一元排序，递归，随机抽样，故障和故障处理，以及对Oracle的黑盒访问。预言机是概率函数，在不同的调用之间保持隐藏状态。为此，我们提出了生成概率系统的语义域中定义的语言的运营商。我们证明了这些运营商是参数化的，并推导出一个关系程序逻辑推理程序参数。几个例子表明，我们的语言是适合进行密码证明。
This paper presents a shallow embedding of a probabilistic functional programming language in higher order logic. The language features monadic sequencing, recursion, random sampling, failures and failure handling, and black-box access to oracles. Oracles are probabilistic functions which maintain hidden state between different invocations. To that end, we propose generative probabilistic systems as the semantic domain in which the operators of the language are defined. We prove that these operators are parametric and derive a relational program logic for reasoning about programs from parametricity. Several examples demonstrate that our language is suitable for conducting cryptographic proofs.
概率系统类型的形式化层次结构 - Proof Pearl
DOI：
10.1007/978-3-319-22102-1_13
发表时间：
2015
期刊：
影响因子：
--
作者：
Johannes Hölzl;Andreas Lochbihler
通讯作者：
Andreas Lochbihler
基础可扩展核心递归：证明助理的观点
DOI：
10.1145/2784731.2784732
发表时间：
2015
期刊：
Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
Jasmin Christian Blanchette;Andrei Popescu;Dmitriy Traytel
通讯作者：
Dmitriy Traytel