A Verified Compiler for Probability Density Functions
A Verified Compiler for Probability Density Functions
复制标题
经过验证的概率密度函数编译器
DOI：
10.1007/978-3-662-46669-8_4
复制
发表时间：
2015
期刊：
影响因子：
--
通讯作者：
Tobias Nipkow
中科院分区：
文献类型：
--
作者：
Manuel Eberl;Johannes Hölzl;Tobias Nipkow
Bhatet等人开发了一个归纳编译器，它可以计算概率空间的密度函数，这些概率空间由概率函数语言中的程序描述。我们实现了这样的编译器的修改版本，这种语言的定理证明器Isabelle，并给出了一个正式的证明其可靠性w。R. t.源语言和目标语言的语义。与Isabelle的归纳谓词代码生成一起，这产生了一个完全验证的，可执行的密度编译器。证明分两步完成：首先，定义一个抽象编译器，它使用直接在定理证明器的逻辑中建模的抽象函数，并证明它是正确的。然后，这个编译器被细化为返回目标语言表达式的具体版本。
Bhatet al. developed an inductive compiler that computes density functions for probability spaces described by programs in a probabilistic functional language. We implement such a compiler for a modified version of this language within the theorem prover Isabelle and give a formal proof of its soundness w. r. t. the semantics of the source and target language. Together with Isabelle’s code generation for inductive predicates, this yields a fully verified, executable density compiler. The proof is done in two steps: First, an abstract compiler working with abstract functions modelled directly in the theorem prover’s logic is defined and proved sound. Then, this compiler is refined to a concrete version that returns a target-language expression.
登录
查看更多内容
DOI：
10.1007/s10817-017-9404-x
发表时间：
2017
期刊：
Journal of Automated Reasoning
影响因子：
--
作者：
Jeremy Avigad;Johannes Hölzl;Luke Serafin
通讯作者：
Luke Serafin
DOI：
10.1145/2103656.2103721
发表时间：
2012
期刊：
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages
影响因子：
--
作者：
Sooraj Bhat;Ashish Agarwal;R. Vuduc;Alexander G. Gray
通讯作者：
Alexander G. Gray
随机关系:马尔可夫转移系统的基础
影响因子：
3.5
作者：
E. Doberkat
通讯作者：
E. Doberkat
影响因子：
0.7
作者：
Fric, Roman;Papco, Martin
通讯作者：
Papco, Martin
DOI：
10.1007/978-3-642-28756-5_47
发表时间：
2012
期刊：
--
影响因子：
--
作者：
Basler G
通讯作者：
Basler G