{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:15Z","timestamp":1780994655856,"version":"3.54.1"},"reference-count":38,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T00:00:00Z","timestamp":1686009600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["2106559"],"award-info":[{"award-number":["2106559"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,6,6]]},"abstract":"<jats:p>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.<\/jats:p>","DOI":"10.1145\/3591245","type":"journal-article","created":{"date-parts":[[2023,6,6]],"date-time":"2023-06-06T20:06:24Z","timestamp":1686081984000},"page":"615-637","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Verified Density Compilation for a Probabilistic Programming Language"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5692-3347","authenticated-orcid":false,"given":"Joseph","family":"Tassarotti","sequence":"first","affiliation":[{"name":"New York University, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2574-7883","authenticated-orcid":false,"given":"Jean-Baptiste","family":"Tristan","sequence":"additional","affiliation":[{"name":"Amazon Web Services, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,6,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3297858.3304019"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386009"},{"key":"e_1_2_1_3_1","unstructured":"Matthew R. Becker. 2016. NUTS Sampler Broken (stan-dev\/stan issue #2178). https:\/\/github.com\/stan-dev\/stan\/issues\/2178 \t\t\t\t  Matthew R. Becker. 2016. NUTS Sampler Broken (stan-dev\/stan issue #2178). https:\/\/github.com\/stan-dev\/stan\/issues\/2178"},{"key":"e_1_2_1_4_1","unstructured":"Michael Betancourt. 2018. A Conceptual Introduction to Hamiltonian Monte Carlo. arxiv:1701.02434. \t\t\t\t  Michael Betancourt. 2018. A Conceptual Introduction to Hamiltonian Monte Carlo. arxiv:1701.02434."},{"key":"e_1_2_1_5_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems, Nir Piterman and Scott A","author":"Bhat Sooraj","unstructured":"Sooraj Bhat , Johannes Borgstr\u00f6m , Andrew D. Gordon , and Claudio Russo . 2013. Deriving Probability Density Functions from Probabilistic Functional Programs . In Tools and Algorithms for the Construction and Analysis of Systems, Nir Piterman and Scott A . Smolka (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 508\u2013522. isbn:978-3-642-36742-7 Sooraj Bhat, Johannes Borgstr\u00f6m, Andrew D. Gordon, and Claudio Russo. 2013. Deriving Probability Density Functions from Probabilistic Functional Programs. In Tools and Algorithms for the Construction and Analysis of Systems, Nir Piterman and Scott A. Smolka (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 508\u2013522. isbn:978-3-642-36742-7"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/s11786-014-0181-1"},{"key":"e_1_2_1_7_1","volume-title":"Programming Languages and Systems - 20th European Symposium on Programming, ESOP","author":"Borgstr\u00f6m Johannes","year":"2011","unstructured":"Johannes Borgstr\u00f6m , Andrew D. Gordon , Michael Greenberg , James Margetson , and Jurgen Van Gael . 2011. Measure Transformer Semantics for Bayesian Machine Learning . In Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011 , Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings, Gilles Barthe (Ed.) (Lecture Notes in Computer Science , Vol. 6602). Springer, 77\u2013 96 . Johannes Borgstr\u00f6m, Andrew D. Gordon, Michael Greenberg, James Margetson, and Jurgen Van Gael. 2011. Measure Transformer Semantics for Bayesian Machine Learning. In Programming Languages and Systems - 20th European Symposium on Programming, ESOP 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbr\u00fccken, Germany, March 26-April 3, 2011. Proceedings, Gilles Barthe (Ed.) (Lecture Notes in Computer Science, Vol. 6602). Springer, 77\u201396."},{"key":"e_1_2_1_8_1","volume-title":"Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016","author":"Borgstr\u00f6m Johannes","year":"2016","unstructured":"Johannes Borgstr\u00f6m , Ugo Dal Lago , Andrew D. Gordon , and Marcin Szymczak . 2016 . A lambda-calculus foundation for universal probabilistic programming . In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016 , Nara, Japan , September 18-22, 2016, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 33\u201346. Johannes Borgstr\u00f6m, Ugo Dal Lago, Andrew D. Gordon, and Marcin Szymczak. 2016. A lambda-calculus foundation for universal probabilistic programming. In Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, Jacques Garrigue, Gabriele Keller, and Eijiro Sumii (Eds.). ACM, 33\u201346."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.18637\/jss.v076.i01"},{"key":"e_1_2_1_10_1","volume-title":"Programming Languages and Systems - 26th European Symposium on Programming, ESOP","author":"Culpepper Ryan","year":"2017","unstructured":"Ryan Culpepper and Andrew Cobb . 2017. Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring . In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017 , Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Hongseok Yang (Ed.) (Lecture Notes in Computer Science , Vol. 10201). Springer, 368\u2013 392 . Ryan Culpepper and Andrew Cobb. 2017. Contextual Equivalence for Probabilistic Programs with Continuous Random Variables and Scoring. In Programming Languages and Systems - 26th European Symposium on Programming, ESOP 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings, Hongseok Yang (Ed.) (Lecture Notes in Computer Science, Vol. 10201). Springer, 368\u2013392."},{"key":"e_1_2_1_11_1","volume-title":"PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 221\u2013236","author":"Cusumano-Towner Marco F.","unstructured":"Marco F. Cusumano-Towner , Feras A. Saad , Alexander K. Lew , and Vikash K. Mansinghka . 2019. Gen: a general-purpose probabilistic programming system with programmable inference . In PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 221\u2013236 . Marco F. Cusumano-Towner, Feras A. Saad, Alexander K. Lew, and Vikash K. Mansinghka. 2019. Gen: a general-purpose probabilistic programming system with programmable inference. In PLDI 2019: Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, 221\u2013236."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236024.3236057"},{"key":"e_1_2_1_13_1","volume-title":"A Verified Compiler for Probability Density Functions","author":"Eberl Manuel","unstructured":"Manuel Eberl , Johannes H\u00f6lzl , and Tobias Nipkow . 2015. A Verified Compiler for Probability Density Functions . In Programming Languages and Systems, Jan Vitek (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 80\u2013104. isbn:978-3-662-46669-8 Manuel Eberl, Johannes H\u00f6lzl, and Tobias Nipkow. 2015. A Verified Compiler for Probability Density Functions. In Programming Languages and Systems, Jan Vitek (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 80\u2013104. isbn:978-3-662-46669-8"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158147"},{"key":"e_1_2_1_15_1","volume-title":"Banaschewski (Ed.) (Lecture Notes in Mathematics","volume":"85","author":"Giry Mich\u00e8le","year":"1982","unstructured":"Mich\u00e8le Giry . 1982 . A Categorical Approach to Probability Theory. In Categorical Aspects of Topology and Analysis, B . Banaschewski (Ed.) (Lecture Notes in Mathematics , Vol. 915). 68\u2013 85 . Mich\u00e8le Giry. 1982. A Categorical Approach to Probability Theory. In Categorical Aspects of Topology and Analysis, B. Banaschewski (Ed.) (Lecture Notes in Mathematics, Vol. 915). 68\u201385."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290348"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.5555\/3329995.3330072"},{"key":"e_1_2_1_18_1","first-page":"1593","article-title":"The No-U-Turn Sampler: Adaptively Setting Path Lengths in Hamiltonian Monte Carlo","volume":"15","author":"Hoffman Matthew D.","year":"2014","unstructured":"Matthew D. Hoffman and Andrew Gelman . 2014 . The No-U-Turn Sampler: Adaptively Setting Path Lengths in Hamiltonian Monte Carlo . Journal of Machine Learning Research , 15 , 47 (2014), 1593 \u2013 1623 . http:\/\/jmlr.org\/papers\/v15\/hoffman14a.html Matthew D. Hoffman and Andrew Gelman. 2014. The No-U-Turn Sampler: Adaptively Setting Path Lengths in Hamiltonian Monte Carlo. Journal of Machine Learning Research, 15, 47 (2014), 1593\u20131623. http:\/\/jmlr.org\/papers\/v15\/hoffman14a.html","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_2_1_19_1","volume-title":"ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 337\u2013363","author":"Huang Daniel","year":"2016","unstructured":"Daniel Huang and Greg Morrisett . 2016 . An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages. In Programming Languages and Systems - 25th European Symposium on Programming , ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 337\u2013363 . Daniel Huang and Greg Morrisett. 2016. An Application of Computable Distributions to the Semantics of Probabilistic Programming Languages. In Programming Languages and Systems - 25th European Symposium on Programming, ESOP 2016, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 2-8, 2016, Proceedings. 337\u2013363."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062375"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the Fourth Annual Symposium on Logic in Computer Science. IEEE Press, 186\u2013195","author":"Jones C.","year":"1861","unstructured":"C. Jones and G. Plotkin . 1989. A Probabilistic Powerdomain of Evaluations . In Proceedings of the Fourth Annual Symposium on Logic in Computer Science. IEEE Press, 186\u2013195 . isbn:08 1861 9546 C. Jones and G. Plotkin. 1989. A Probabilistic Powerdomain of Evaluations. In Proceedings of the Fourth Annual Symposium on Logic in Computer Science. IEEE Press, 186\u2013195. isbn:0818619546"},{"key":"e_1_2_1_22_1","unstructured":"S. Kazemi and D. Poole. 2016. Knowledge Compilation for Lifted Probabilistic Inference: Compiling to a Low-Level Language. In KR. \t\t\t\t  S. Kazemi and D. Poole. 2016. Knowledge Compilation for Lifted Probabilistic Inference: Compiling to a Low-Level Language. In KR."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535841"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/1538788.1538814"},{"key":"e_1_2_1_26_1","volume-title":"Proceedings of the ACM on Programming Languages, 4, POPL","author":"Lew Alexander K.","year":"2020","unstructured":"Alexander K. Lew , Marco F. Cusumano-Towner , Benjamin Sherman , Michale Carbin , and Vikash K. Mansinghka . 2020. Trace types and denotational semantics for sound programmable inference in probabilistic languages . Proceedings of the ACM on Programming Languages, 4, POPL ( 2020 ), Article 19, Jan., 32 pages. Alexander K. Lew, Marco F. Cusumano-Towner, Benjamin Sherman, Michale Carbin, and Vikash K. Mansinghka. 2020. Trace types and denotational semantics for sound programmable inference in probabilistic languages. Proceedings of the ACM on Programming Languages, 4, POPL (2020), Article 19, Jan., 32 pages."},{"key":"e_1_2_1_27_1","unstructured":"ProbCompCert Development Team. 2023. ProbCompCert Git Repository. https:\/\/github.com\/jtassarotti\/probcompcert \t\t\t\t  ProbCompCert Development Team. 2023. ProbCompCert Git Repository. https:\/\/github.com\/jtassarotti\/probcompcert"},{"key":"e_1_2_1_28_1","doi-asserted-by":"crossref","unstructured":"Norman Ramsey and Avi Pfeffer. 2002. Stochastic lambda calculus and monads of probability distributions. In POPL. 154\u2013165. \t\t\t\t  Norman Ramsey and Avi Pfeffer. 2002. Stochastic lambda calculus and monads of probability distributions. In POPL. 154\u2013165.","DOI":"10.1145\/565816.503288"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1239\/jap\/1032192546"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7760173"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90003-1"},{"key":"e_1_2_1_32_1","doi-asserted-by":"crossref","first-page":"1","DOI":"10.1145\/3158148","article-title":"Denotational validation of higher-order Bayesian inference","volume":"2","author":"Scibior A.","year":"2018","unstructured":"A. Scibior , Ohad Kammar , Matthijs V\u00e1k\u00e1r , S. Staton , H. Yang , Yufei Cai , K. Ostermann , Sean K. Moss , C. Heunen , and Z. Ghahramani . 2018 . Denotational validation of higher-order Bayesian inference . Proceedings of the ACM on Programming Languages , 2 (2018), 1 \u2013 29 . A. Scibior, Ohad Kammar, Matthijs V\u00e1k\u00e1r, S. Staton, H. Yang, Yufei Cai, K. Ostermann, Sean K. Moss, C. Heunen, and Z. Ghahramani. 2018. Denotational validation of higher-order Bayesian inference. Proceedings of the ACM on Programming Languages, 2 (2018), 1 \u2013 29.","journal-title":"Proceedings of the ACM on Programming Languages"},{"key":"e_1_2_1_33_1","unstructured":"Stan Development Team. 2023. Stan Language Reference Manual (v. 2.31). https:\/\/mc-stan.org\/docs\/2_31\/reference-manual\/ \t\t\t\t  Stan Development Team. 2023. Stan Language Reference Manual (v. 2.31). https:\/\/mc-stan.org\/docs\/2_31\/reference-manual\/"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_32"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.7709874"},{"key":"e_1_2_1_36_1","volume-title":"Augur: Data-Parallel Probabilistic Modeling. In Advances in Neural Information Processing Systems 27","author":"Tristan Jean-Baptiste","year":"2014","unstructured":"Jean-Baptiste Tristan , Daniel Huang , Joseph Tassarotti , Adam C Pocock , Stephen Green , and Guy L Steele . 2014 . Augur: Data-Parallel Probabilistic Modeling. In Advances in Neural Information Processing Systems 27 , Z. Ghahramani, M. Welling, C. Cortes, N. D. Lawrence, and K. Q. Weinberger (Eds.). Neural Information Processing Systems Foundation . Jean-Baptiste Tristan, Daniel Huang, Joseph Tassarotti, Adam C Pocock, Stephen Green, and Guy L Steele. 2014. Augur: Data-Parallel Probabilistic Modeling. In Advances in Neural Information Processing Systems 27, Z. Ghahramani, M. Welling, C. Cortes, N. D. Lawrence, and K. Q. Weinberger (Eds.). Neural Information Processing Systems Foundation."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/3236782"},{"key":"e_1_2_1_38_1","volume-title":"Swift: Compiled Inference for Probabilistic Programming Languages. In IJCAI.","author":"Wu Yi","year":"2016","unstructured":"Yi Wu , Lei Li , S. Russell , and Rastislav Bod\u00edk . 2016 . Swift: Compiled Inference for Probabilistic Programming Languages. In IJCAI. Yi Wu, Lei Li, S. Russell, and Rastislav Bod\u00edk. 2016. Swift: Compiled Inference for Probabilistic Programming Languages. In IJCAI."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591245","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3591245","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:47:47Z","timestamp":1750178867000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3591245"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,6,6]]},"references-count":38,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2023,6,6]]}},"alternative-id":["10.1145\/3591245"],"URL":"https:\/\/doi.org\/10.1145\/3591245","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,6,6]]},"assertion":[{"value":"2023-06-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}