{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T16:40:32Z","timestamp":1760028032809,"version":"3.41.0"},"publisher-location":"New York, NY, USA","reference-count":38,"publisher":"ACM","license":[{"start":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T00:00:00Z","timestamp":1673395200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100001691","name":"Japan Society for the Promotion of Science","doi-asserted-by":"publisher","award":["KAKENHI 22H00520"],"award-info":[{"award-number":["KAKENHI 22H00520"]}],"id":[{"id":"10.13039\/501100001691","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":[],"published-print":{"date-parts":[[2023,1,11]]},"DOI":"10.1145\/3573105.3575691","type":"proceedings-article","created":{"date-parts":[[2023,1,11]],"date-time":"2023-01-11T22:27:08Z","timestamp":1673476028000},"page":"3-16","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":7,"title":["Semantics of Probabilistic Programs using s-Finite Kernels in Coq"],"prefix":"10.1145","author":[{"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[{"name":"AIST, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Cyril","family":"Cohen","sequence":"additional","affiliation":[{"name":"Inria, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Ayumu","family":"Saito","sequence":"additional","affiliation":[{"name":"Tokyo Institute of Technology, Japan"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,1,11]]},"reference":[{"key":"e_1_3_2_1_1_1","volume-title":"Assia Mahboubi, Damien Rouhling, Pierre Roux, Kazuhiko Sakaguchi, Zachary Stone, Pierre-Yves Strub, and Laurent Th\u00e9ry.","author":"Affeldt Reynald","year":"2022","unstructured":"Reynald Affeldt, Yves Bertot, Cyril Cohen Marie Kerjean, Assia Mahboubi, Damien Rouhling, Pierre Roux, Kazuhiko Sakaguchi, Zachary Stone, Pierre-Yves Strub, and Laurent Th\u00e9ry. 2022. MathComp-Analysis: Mathematical Components compliant Analysis Library. https:\/\/github.com\/math-comp\/analysis Since 2017. Version 0.5.4"},{"key":"e_1_3_2_1_2_1","unstructured":"Reynald Affeldt and Cyril Cohen. 2022. Measure Construction by Extension in Dependent Type Theory with Application to Integration. arxiv:2209.02345."},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-51054-1_1"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.6092\/issn.1972-5787"},{"key":"e_1_3_2_1_5_1","unstructured":"Reynald Affeldt Cyril Cohen and Ayumu Saito. 2022. Semantics of Probabilistic Programs using s-Finite Kernels in Coq. MathComp-Analysis Pull Request. https:\/\/github.com\/math-comp\/analysis\/pull\/749"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000137"},{"key":"e_1_3_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-013-9298-1"},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-33636-3_9"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.002"},{"key":"e_1_3_2_1_10_1","volume-title":"Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees. In 33rd AAAI Conference on Artificial Intelligence (AAAI","author":"Bagnall Alexander","year":"2019","unstructured":"Alexander Bagnall and Gordon Stewart. 2019. Certifying the True Error: Machine Learning in Coq with Verified Generalization Guarantees. In 33rd AAAI Conference on Artificial Intelligence (AAAI 2019). Association for the Advancement of Artificial Intelligence (AAAI), 2662\u20132669. https:\/\/par.nsf.gov\/servlets\/purl\/10138645"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89884-1_6"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129521000165"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951942"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.34"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03359-9_23"},{"key":"e_1_3_2_1_17_1","volume-title":"Workshop on Languages for Inference (LAFI 2019","author":"Heimerdinger Matthew","year":"2019","unstructured":"Matthew Heimerdinger and Chung-chieh Shan. 2019. Verified Equational Reasoning on a Little Language of Measures. Workshop on Languages for Inference (LAFI 2019), Cascais, Portugal, January 15, 2019."},{"key":"e_1_3_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99461-7_4"},{"volume-title":"Formal verification of probabilistic algorithms. Ph. D. Dissertation. Computer Laboratory","author":"Hurd Joe","key":"e_1_3_2_1_20_1","unstructured":"Joe Hurd. 2001. Formal verification of probabilistic algorithms. Ph. D. Dissertation. Computer Laboratory, University of Cambridge."},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"volume-title":"Lectures on the Poisson Process","author":"Last G\u00fcnter","key":"e_1_3_2_1_22_1","unstructured":"G\u00fcnter Last and Mathew Penrose. 2017. Lectures on the Poisson Process. Cambridge University Press."},{"key":"e_1_3_2_1_23_1","unstructured":"Daniel Li. 2016. Int\u00e9gration et applications\u2014Cours et exercices corrig\u00e9s. Eyrolles."},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","unstructured":"Assia Mahboubi and Enrico Tassi. 2021. Mathematical Components. Zenodo. https:\/\/doi.org\/10.5281\/zenodo.4457887 10.5281\/zenodo.4457887","DOI":"10.5281\/zenodo.4457887"},{"key":"e_1_3_2_1_25_1","volume-title":"Verifiable and Reusable Conditioning. Ph. D. Dissertation. School of Informatics, Computing, and Engineering","author":"Narayanan Praveen","year":"2022","unstructured":"Praveen Narayanan. 2019. Verifiable and Reusable Conditioning. Ph. D. Dissertation. School of Informatics, Computing, and Engineering, Indiana University. https:\/\/scholarworks.iu.edu\/dspace\/handle\/2022\/24645w"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-29604-3_5"},{"volume-title":"Radon-Nikod\u00fdm derivatives and disintegration for s-finite measures: some semantic bases for probabilistic metaprogramming. Seminar 113: Metaprogramming for Statistical Machine Learning","author":"Ong Luke","key":"e_1_3_2_1_27_1","unstructured":"Luke Ong and Matthijs V\u00e1k\u00e1r. 2018. Radon-Nikod\u00fdm derivatives and disintegration for s-finite measures: some semantic bases for probabilistic metaprogramming. Seminar 113: Metaprogramming for Statistical Machine Learning, Shonan Village Centre."},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"crossref","unstructured":"D. Pollard. 2002. A user\u2019s guide to measure theoretic probability. CUP.","DOI":"10.1017\/CBO9780511811555"},{"key":"e_1_3_2_1_29_1","unstructured":"Chung-chieh Shan. 2018. Equational reasoning for probabilistic programming. POPL TutorialFest."},{"key":"e_1_3_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_32"},{"key":"e_1_3_2_1_31_1","doi-asserted-by":"publisher","unstructured":"Sam Staton. 2020. Probabilistic Programs as Measures. 43\u201374. https:\/\/doi.org\/10.1017\/9781108770750.003 Chapter in barthes2020cup 10.1017\/9781108770750.003","DOI":"10.1017\/9781108770750.003"},{"key":"e_1_3_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935313"},{"key":"e_1_3_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3437992.3439917"},{"key":"e_1_3_2_1_34_1","unstructured":"The Coq Development Team. 2022. The Coq Proof Assistant Reference Manual. Available at https:\/\/coq.inria.fr"},{"key":"e_1_3_2_1_35_1","unstructured":"The Coq Development Team. 2022. Reversible Coercions. Section in coq. https:\/\/coq.inria.fr\/refman\/addendum\/implicit-coercions.html#reversible-coercions Coq Pull Request"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","unstructured":"Matthijs V\u00e1k\u00e1r and Luke Ong. 2018. On S-Finite Measures and Kernels. https:\/\/doi.org\/10.48550\/ARXIV.1810.01837","DOI":"10.48550\/ARXIV.1810.01837"},{"key":"e_1_3_2_1_37_1","volume-title":"7th International Conference on Artificial Intelligence and Statistics (AISTATS 2014) Reykjavik, Iceland, April 22\u201325, 2014 (JMLR Workshop and Conference Proceedings","volume":"1032","author":"Wood Frank D.","unstructured":"Frank D. Wood, Jan-Willem van de Meent, and Vikash Mansinghka. 2014. A New Approach to Probabilistic Programming Inference. In 7th International Conference on Artificial Intelligence and Statistics (AISTATS 2014) Reykjavik, Iceland, April 22\u201325, 2014 (JMLR Workshop and Conference Proceedings, Vol. 33). JMLR.org, 1024\u20131032. http:\/\/proceedings.mlr.press\/v33\/wood14.html"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498677"}],"event":{"name":"CPP '23: 12th ACM SIGPLAN International Conference on Certified Programs and Proofs","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages"],"location":"Boston MA USA","acronym":"CPP '23"},"container-title":["Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575691","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3573105.3575691","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:45:38Z","timestamp":1750178738000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3573105.3575691"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,1,11]]},"references-count":38,"alternative-id":["10.1145\/3573105.3575691","10.1145\/3573105"],"URL":"https:\/\/doi.org\/10.1145\/3573105.3575691","relation":{},"subject":[],"published":{"date-parts":[[2023,1,11]]},"assertion":[{"value":"2023-01-11","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}