Semantics of Probabilistic Programs using s-Finite Kernels in Coq
Semantics of Probabilistic Programs using s-Finite Kernels in Coq
复制标题
在 Coq 中使用 s-有限核的概率程序语义
DOI：
10.1145/3573105.3575691
复制
发表时间：
2023
期刊：
影响因子：
--
通讯作者：
Saito Ayumu
中科院分区：
文献类型：
--
作者：
Affeldt Reynald;Cohen Cyril;Saito Ayumu
Probabilistic编程语言用于编写概率 模型来进行概率推断。一些严格的 最近已经提出了语义学， 对概率程序进行形式化验证。 在本文中，我们推广了一个已有的测度形式化， s-有限核积分理论一种数学结构 在概率的语义中解释类型判断， 编程语言.由此产生的库使得有可能 关于概率程序变换的形式化推理， 他们的处决。
Probabilistic programming languages are used to write probabilistic models to make probabilistic inferences. A number of rigorous semantics have recently been proposed that are now available to carry out formal verification of probabilistic programs. In this paper, we extend an existing formalization of measure and integration theory with s-finite kernels, a mathematical structure to interpret typing judgments in the semantics of a probabilistic programming language. The resulting library makes it possible to reason formally about transformations of probabilistic programs and their execution.
登录
查看更多内容
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
Hakaru 中程序转换的概率推理（系统描述）
DOI：
10.1007/978-3-319-29604-3_5
发表时间：
2016
期刊：
IEEE INFOCOM 2009
影响因子：
--
作者：
P. Narayanan;J. Carette;Wren Romano;Chung;R. Zinkov
通讯作者：
R. Zinkov
DOI：
10.1609/aaai.v33i01.33012662
发表时间：
2019-07
期刊：
ArXiv
影响因子：
--
作者：
Alexander Bagnall;Gordon Stewart
通讯作者：
Alexander Bagnall;Gordon Stewart
DOI：
10.1017/s0960129521000165
发表时间：
2019
期刊：
Math. Struct. Comput. Sci.
影响因子：
--
作者：
Florian Faissole;Bas Spitters
通讯作者：
Bas Spitters