Verified Density Compilation for a Probabilistic Programming Language
Verified Density Compilation for a Probabilistic Programming Language
复制标题
概率编程语言的验证密度编译
DOI：
10.1145/3591245
复制
发表时间：
2023
影响因子：
--
通讯作者：
Tristan, Jean-Baptiste
中科院分区：
文献类型：
--
作者：
Tassarotti, Joseph;Tristan, Jean-Baptiste
本文介绍了一个用于Stan概率编程语言(PPL)子集的编译器ProbCompCert，其中几个关键的编译器遍已经使用Coq证明助手进行了形式化验证。由于ppls的概率性质，其编译器中的错误很难检测和修复，这使得验证成为一种有趣的可能性。然而，证明PPL编译的正确性需要新的技术，因为编译器对PPL执行的某些转换与其他类型的语言有很大的不同。本文描述了验证这种转换的技术及其在ProbCompCert中的应用。在验证ProbCompCert的过程中，我们在Stan语言参考手册中发现了一个与关键语言构造的语义和实现相关的错误。
This paper presents ProbCompCert, a compiler for a subset of the Stan probabilistic programming language (PPL), in which several key compiler passes have been formally verified using the Coq proof assistant. Because of the probabilistic nature of PPLs, bugs in their compilers can be difficult to detect and fix, making verification an interesting possibility. However, proving correctness of PPL compilation requires new techniques because certain transformations performed by compilers for PPLs are quite different from other kinds of languages. This paper describes techniques for verifying such transformations and their application in ProbCompCert. In the course of verifying ProbCompCert, we found an error in the Stan language reference manual related to the semantics and implementation of a key language construct.
登录
查看更多内容
DOI：
10.1145/2951913.2951942
发表时间：
2015-12
期刊：
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming
影响因子：
--
作者：
J. Borgström;Ugo Dal Lago;A. Gordon;Marcin Szymczak
通讯作者：
J. Borgström;Ugo Dal Lago;A. Gordon;Marcin Szymczak
DOI：
10.1109/lics.2017.8005137
发表时间：
2017
期刊：
--
影响因子：
--
作者：
Heunen C
通讯作者：
Heunen C
影响因子：
0.8
作者：
Boldo, Sylvie;Lelay, Catherine;Melquiond, Guillaume
通讯作者：
Melquiond, Guillaume
影响因子：
5.8
作者：
Carpenter, Bob;Gelman, Andrew;Riddell, Allen
通讯作者：
Riddell, Allen
用于提升概率推理的知识编译：编译为低级语言
DOI：
--
发表时间：
2016
期刊：
International Conference on Principles of Knowledge Representation and Reasoning
影响因子：
--
作者：
Seyed Mehran Kazemi;D. Poole
通讯作者：
D. Poole