{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T19:13:31Z","timestamp":1773429211833,"version":"3.50.1"},"publisher-location":"Singapore","reference-count":42,"publisher":"Springer Nature Singapore","isbn-type":[{"value":"9789819535842","type":"print"},{"value":"9789819535859","type":"electronic"}],"license":[{"start":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T00:00:00Z","timestamp":1761868800000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2025,10,31]],"date-time":"2025-10-31T00:00:00Z","timestamp":1761868800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2026]]},"DOI":"10.1007\/978-981-95-3585-9_3","type":"book-chapter","created":{"date-parts":[[2025,10,30]],"date-time":"2025-10-30T06:07:04Z","timestamp":1761804424000},"page":"44-64","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["A Formal Foundation for\u00a0Equational Reasoning on\u00a0Probabilistic Programs"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-2327-953X","authenticated-orcid":false,"given":"Reynald","family":"Affeldt","sequence":"first","affiliation":[]},{"given":"Yoshihiro","family":"Ishiguro","sequence":"additional","affiliation":[]},{"given":"Zachary","family":"Stone","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2025,10,31]]},"reference":[{"issue":"3","key":"3_CR1","doi-asserted-by":"publisher","first-page":"28","DOI":"10.1007\/S10817-023-09671-5","volume":"67","author":"R Affeldt","year":"2023","unstructured":"Affeldt, R., Cohen, C.: Measure construction by extension in dependent type theory with application to integration. J. Autom. Reason. 67(3), 28 (2023). https:\/\/doi.org\/10.1007\/S10817-023-09671-5","journal-title":"J. Autom. Reason."},{"issue":"1","key":"3_CR2","doi-asserted-by":"publisher","first-page":"43","DOI":"10.6092\/issn.1972-5787\/8124","volume":"11","author":"R Affeldt","year":"2018","unstructured":"Affeldt, R., Cohen, C., Rouhling, D.: Formalization techniques for asymptotic reasoning in classical analysis. J. Formaliz. Reason. 11(1), 43\u201376 (2018). https:\/\/doi.org\/10.6092\/issn.1972-5787\/8124","journal-title":"J. Formaliz. Reason."},{"key":"3_CR3","doi-asserted-by":"publisher","unstructured":"Affeldt, R., Cohen, C., Saito, A.: Semantics of probabilistic programs using s-finite kernels in dependent type theory. ACM Trans. Probab. Mach. Learn. 1(3) (2025). https:\/\/doi.org\/10.1145\/3732291","DOI":"10.1145\/3732291"},{"key":"3_CR4","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796821000137","volume":"31","author":"R Affeldt","year":"2021","unstructured":"Affeldt, R., Garrigue, J., Nowak, D., Saikawa, T.: A trustful monad for axiomatic reasoning with probability and nondeterminism. J. Funct. Program. 31, e17 (2021). https:\/\/doi.org\/10.1017\/S0956796821000137","journal-title":"J. Funct. Program."},{"key":"3_CR5","doi-asserted-by":"publisher","unstructured":"Affeldt, R., Garrigue, J., Saikawa, T.: A practical formalization of monadic equational reasoning in dependent-type theory. J. Funct. Program. 35 (2025). https:\/\/doi.org\/10.1017\/S0956796824000157","DOI":"10.1017\/S0956796824000157"},{"key":"3_CR6","unstructured":"Affeldt, R., Ishiguro, Y., Stone, Z.: Equational reasoning for probabilistic programming in Rocq\u2014accompanying development. MathComp-Analysis Pull Request. https:\/\/github.com\/math-comp\/analysis\/pull\/1712"},{"key":"3_CR7","doi-asserted-by":"publisher","unstructured":"Affeldt, R., Stone, Z.: A comprehensive overview of the Lebesgue differentiation theorem in Coq. In: 15th International Conference on Interactive Theorem Proving (ITP 2024), 9\u201314 September 2024, Tbilisi, Georgia. LIPIcs, vol.\u00a0309, pp. 5:1\u20135:19. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2024). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2024.5","DOI":"10.4230\/LIPICS.ITP.2024.5"},{"issue":"8","key":"3_CR8","doi-asserted-by":"publisher","first-page":"568","DOI":"10.1016\/j.scico.2007.09.002","volume":"74","author":"P Audebaud","year":"2009","unstructured":"Audebaud, P., Paulin-Mohring, C.: Proofs of randomized algorithms in Coq. Sci. Comput. Program. 74(8), 568\u2013589 (2009). https:\/\/doi.org\/10.1016\/j.scico.2007.09.002","journal-title":"Sci. Comput. Program."},{"issue":"4","key":"3_CR9","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/S10817-017-9404-X","volume":"59","author":"J Avigad","year":"2017","unstructured":"Avigad, J., H\u00f6lzl, J., Serafin, L.: A formally verified proof of the central limit theorem. J. Autom. Reason. 59(4), 389\u2013423 (2017). https:\/\/doi.org\/10.1007\/S10817-017-9404-X","journal-title":"J. Autom. Reason."},{"key":"3_CR10","unstructured":"Bingham, E., et al.: Pyro: deep universal probabilistic programming. J. Mach. Learn. Res. 20, 28:1\u201328:6 (2019)"},{"key":"3_CR11","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a formalization of real analysis for Coq. http:\/\/coquelicot.saclay.inria.fr\/html\/Coquelicot.Coquelicot.html. Accessed 19 Mar 2025"},{"issue":"9","key":"3_CR12","doi-asserted-by":"publisher","first-page":"1177","DOI":"10.1038\/nbt0904-1177","volume":"22","author":"SR Eddy","year":"2004","unstructured":"Eddy, S.R.: What is Bayesian statistics? Nat. Biotechnol. 22(9), 1177\u20131178 (2004)","journal-title":"Nat. Biotechnol."},{"key":"3_CR13","doi-asserted-by":"publisher","unstructured":"Gou\u00ebzel, S.: A formalization of the change of variables formula for integrals in mathlib. In: 15th International Conference on Intelligent Computer Mathematics (CICM 2022), Tbilisi, Georgia, 19\u201323 September 2022. Lecture Notes in Computer Science, vol. 13467, pp. 3\u201318. Springer (2022). https:\/\/doi.org\/10.1007\/978-3-031-16681-5_1","DOI":"10.1007\/978-3-031-16681-5_1"},{"key":"3_CR14","doi-asserted-by":"publisher","unstructured":"Haselwarter, P.G., et al.: SSProve: a foundational framework for modular cryptographic proofs in Coq. ACM Trans. Program. Lang. Syst. 45(3), 15:1\u201315:61 (2023). https:\/\/doi.org\/10.1145\/3594735","DOI":"10.1145\/3594735"},{"key":"3_CR15","unstructured":"Heimerdinger, M., Shan, C.: Verified equational reasoning on a little language of measures. In: Workshop on Languages for Inference (LAFI 2019), Cascais, Portugal, 15 January 2019 (2019)"},{"key":"3_CR16","doi-asserted-by":"publisher","unstructured":"Heunen, C., Kammar, O., Staton, S., Yang, H.: A convenient category for higher-order probability theory. In: 32nd Annual ACM\/IEEE Symposium on Logic in Computer Science (LICS 2017), Reykjavik, Iceland, 20\u201323 June 2017, pp. 1\u201312. IEEE Computer Society (2017). https:\/\/doi.org\/10.1109\/LICS.2017.8005137","DOI":"10.1109\/LICS.2017.8005137"},{"key":"3_CR17","doi-asserted-by":"publisher","DOI":"10.1016\/J.SCICO.2023.102993","volume":"230","author":"M Hirata","year":"2023","unstructured":"Hirata, M., Minamide, Y., Sato, T.: Program logic for higher-order probabilistic programs in Isabelle\/HOL. Sci. Comput. Program. 230, 102993 (2023). https:\/\/doi.org\/10.1016\/J.SCICO.2023.102993","journal-title":"Sci. Comput. Program."},{"key":"3_CR18","doi-asserted-by":"publisher","unstructured":"Hirata, M., Minamide, Y., Sato, T.: Semantic foundations of higher-order probabilistic programs in Isabelle\/HOL. In: 14th International Conference on Interactive Theorem Proving (ITP 2023), 31 July\u20134 August 2023, Bia\u0142ystok, Poland. LIPIcs, vol.\u00a0268, pp. 18:1\u201318:18. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2023). https:\/\/doi.org\/10.4230\/LIPICS.ITP.2023.18","DOI":"10.4230\/LIPICS.ITP.2023.18"},{"key":"3_CR19","unstructured":"Hurd, J.: Formal verification of probabilistic algorithms. Ph.D. thesis, Computer Laboratory, University of Cambridge (2001)"},{"key":"3_CR20","doi-asserted-by":"publisher","unstructured":"Ishiguro, Y., Affeldt, R.: The Radon-Nikod\u00fdm theorem and the Lebesgue-Stieltjes measure in Coq. Comput. Softw. 41(2), 41\u201349 (2024). https:\/\/doi.org\/10.11309\/jssst.41.2_41","DOI":"10.11309\/jssst.41.2_41"},{"key":"3_CR21","doi-asserted-by":"crossref","unstructured":"Kadets, V.: A Course in Functional Analysis and Measure Theory. Universitext, Springer (2018)","DOI":"10.1007\/978-3-319-92004-7"},{"issue":"2","key":"3_CR22","doi-asserted-by":"publisher","first-page":"281","DOI":"10.1007\/s10817-018-9463-7","volume":"62","author":"A Mahboubi","year":"2018","unstructured":"Mahboubi, A., Melquiond, G., Sibut-Pinote, T.: Formally verified approximations of definite integrals. J. Autom. Reason. 62(2), 281\u2013300 (2018). https:\/\/doi.org\/10.1007\/s10817-018-9463-7","journal-title":"J. Autom. Reason."},{"key":"3_CR23","unstructured":"MathComp-Analysis: MathComp-Analysis: Mathematical Components compliant analysis library (2017). https:\/\/github.com\/math-comp\/analysis. Authors: Reynald Affeldt, Yves Bertot, Alessandro Bruni, Cyril Cohen, Marie Kerjean, Assia Mahboubi, Damien Rouhling, Pierre Roux, Kazuhiko Sakaguchi, Zachary Stone, Pierre-Yves Strub, and Laurent Th\u00e9ry. Last stable version: 1.13.0 (2025)"},{"key":"3_CR24","unstructured":"Monae: Monadic effects and equational reasonig in Rocq (2018). https:\/\/github.com\/affeldt-aist\/monae. Authors: Reynald Affeldt, David Nowak, Takafumi Saikawa, Jacques Garrigue, Ayumu Saito, Celestine Sauvage, and Kazunari Tanaka. Last stable release: 0.9.1 (2025)"},{"key":"3_CR25","unstructured":"Narayanan, P.: Verifiable and reusable conditioning. Ph.D. thesis, Indiana University (2019)"},{"key":"3_CR26","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"62","DOI":"10.1007\/978-3-319-29604-3_5","volume-title":"Functional and Logic Programming","author":"P Narayanan","year":"2016","unstructured":"Narayanan, P., Carette, J., Romano, W., Shan, C., Zinkov, R.: Probabilistic inference by program transformation in Hakaru (system description). In: Kiselyov, O., King, A. (eds.) FLOPS 2016. LNCS, vol. 9613, pp. 62\u201379. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-29604-3_5"},{"key":"3_CR27","unstructured":"Rouhling, D.: Formalisation Tools for Classical Analysis\u2014A Case Study in Control Theory. Ph.D. thesis, Universit\u00e9 C\u00f4te d\u2019Azur (2019)"},{"key":"3_CR28","unstructured":"Rudin, W.: Principles of Mathematical Analysis, 3rd edn. McGraw-Hill (1976)"},{"key":"3_CR29","doi-asserted-by":"publisher","unstructured":"Saito, A., Affeldt, R.: Experimenting with an intrinsically-typed probabilistic programming language in Coq. In: 21st Asian Symposium on Programming Languages and Systems (APLAS 2023), Taipei, Taiwan, 26\u201329 November. Lecture Notes in Computer Science, vol. 14405, pp. 182\u2013202. Springer (2023). https:\/\/doi.org\/10.1007\/978-981-99-8311-7_9","DOI":"10.1007\/978-981-99-8311-7_9"},{"key":"3_CR30","unstructured":"Sakaguchi, K., Roux, P.: Algebra tactics: ring, field, lra, nra, and psatz tactics for Mathematical Components (2021). https:\/\/github.com\/math-comp\/algebra-tactics. Last stable release: 1.2.6 (2025)"},{"key":"3_CR31","doi-asserted-by":"publisher","unstructured":"Shan, C.: Calculating distributions. In: 20th International Symposium on Principles and Practice of Declarative Programming (PPDP 2018), Frankfurt am Main, Germany, 3\u20135 September 2018, pp. 2:1\u20132:5. ACM (2018). https:\/\/doi.org\/10.1145\/3236950.3236973","DOI":"10.1145\/3236950.3236973"},{"key":"3_CR32","unstructured":"Shan, C.C.: Equational reasoning for probabilistic programming. POPL 2018 TutorialFest (2018). https:\/\/homes.luddy.indiana.edu\/ccshan\/rational\/equational-handout.pdf"},{"key":"3_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"855","DOI":"10.1007\/978-3-662-54434-1_32","volume-title":"Programming Languages and Systems","author":"S Staton","year":"2017","unstructured":"Staton, S.: Commutative semantics for probabilistic programming. In: Yang, H. (ed.) ESOP 2017. LNCS, vol. 10201, pp. 855\u2013879. Springer, Heidelberg (2017). https:\/\/doi.org\/10.1007\/978-3-662-54434-1_32"},{"key":"3_CR34","doi-asserted-by":"publisher","unstructured":"Tassarotti, J., Tristan, J.: Verified density compilation for a probabilistic programming language. Proc. ACM Program. Lang. 7(PLDI), 615\u2013637 (2023). https:\/\/doi.org\/10.1145\/3591245","DOI":"10.1145\/3591245"},{"key":"3_CR35","doi-asserted-by":"publisher","unstructured":"Tassarotti, J., Vajjha, K., Banerjee, A., Tristan, J.: A formal proof of PAC learnability for decision stumps. In: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP 2021), Virtual Event, Denmark, 17\u201319 January 2021, pp. 5\u201317. ACM (2021). https:\/\/doi.org\/10.1145\/3437992.3439917","DOI":"10.1145\/3437992.3439917"},{"key":"3_CR36","unstructured":"The MathComp development team: Mathematical components (2005). https:\/\/github.com\/math-comp\/math-comp. Last stable version: 2.4.0 (2025)"},{"key":"3_CR37","unstructured":"The Rocq Development Team: Custom entries. Inria (2025). Chapter \u201cSyntax extensions and notation scopes\u201d of [38]"},{"key":"3_CR38","unstructured":"The Rocq Development Team: The Rocq Proof Assistant Reference Manual. Inria (2025). https:\/\/rocq-prover.org\/doc\/V9.0.0\/refman\/index.html. Version 9.0.0"},{"key":"3_CR39","unstructured":"The Stan Development Team: Stan modeling language users guide and reference manual (2024). https:\/\/mc-stan.org\/"},{"key":"3_CR40","unstructured":"Wikipedia: Fundamental theorem of calculus (2025). https:\/\/en.wikipedia.org\/wiki\/Fundamental_theorem_of_calculus. Accessed 24 Mar 2025"},{"key":"3_CR41","unstructured":"Wood, F.D., van\u00a0de Meent, J., Mansinghka, V.: A new approach to probabilistic programming inference. In: 7th International Conference on Artificial Intelligence and Statistics (AISTATS 2014), Reykjavik, Iceland, 22\u201325 April 2014. JMLR Workshop and Conference Proceedings, vol.\u00a033, pp. 1024\u20131032. JMLR.org (2014)"},{"key":"3_CR42","doi-asserted-by":"publisher","unstructured":"Zhang, Y., Amin, N.: Reasoning about \u201creasoning about reasoning\u201d: semantics and contextual equivalence for probabilistic programs with nested queries and recursion. Proc. ACM Program. Lang. 6(POPL), 1\u201328 (2022). https:\/\/doi.org\/10.1145\/3498677","DOI":"10.1145\/3498677"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-981-95-3585-9_3","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,3,13]],"date-time":"2026-03-13T18:14:14Z","timestamp":1773425654000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-981-95-3585-9_3"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,31]]},"ISBN":["9789819535842","9789819535859"],"references-count":42,"URL":"https:\/\/doi.org\/10.1007\/978-981-95-3585-9_3","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,31]]},"assertion":[{"value":"31 October 2025","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"The authors have no competing interests to declare that are relevant to the content of this article.","order":1,"name":"Ethics","group":{"name":"EthicsHeading","label":"Disclosure of Interests"}},{"value":"APLAS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Asian Symposium on Programming Languages and Systems","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Bengaluru","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"India","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2025","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"27 June 2025","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"30 June 2025","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"23","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"aplas2025","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/conf.researchr.org\/track\/aplas-2025\/aplas-2025-aplas-2025","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}