{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:17Z","timestamp":1780994537901,"version":"3.54.1"},"reference-count":64,"publisher":"Association for Computing Machinery (ACM)","issue":"PLDI","license":[{"start":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T00:00:00Z","timestamp":1749772800000},"content-version":"vor","delay-in-days":3,"URL":"http:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["2116372,2220408"],"award-info":[{"award-number":["2116372,2220408"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,6,10]]},"abstract":"<jats:p>Exact probabilistic inference is a requirement for many applications of probabilistic programming languages (PPLs) such as in high-consequence settings or verification. However, designing and implementing a PPL with scalable high-performance exact inference is difficult: exact inference engines, much like SAT solvers, are intricate low-level programs that are hard to implement. Due to this implementation challenge, PPLs that support scalable exact inference are restrictive and lack many features of general-purpose languages.<\/jats:p>\n          <jats:p>This paper presents Roulette, the first discrete probabilistic programming language that combines high-performance exact inference with general-purpose language features. Roulette supports a significant subset of Racket, including data structures, first-class functions, surely-terminating recursion, mutable state, modules, and macros, along with probabilistic features such as finitely supported discrete random variables, conditioning, and top-level inference. The key insight is that there is a close connection between exact probabilistic inference and the symbolic evaluation strategy of Rosette. Building on this connection, Roulette generalizes and extends the Rosette solver-aided programming system to reason about probabilistic rather than symbolic quantities. We prove Roulette sound by generalizing a proof of correctness for Rosette to handle probabilities, and demonstrate its scalability and expressivity on a number of examples.<\/jats:p>","DOI":"10.1145\/3729334","type":"journal-article","created":{"date-parts":[[2025,6,13]],"date-time":"2025-06-13T16:02:27Z","timestamp":1749830547000},"page":"2081-2105","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":3,"title":["Roulette: A Language for Expressive, Exact, and Efficient Discrete Probabilistic Programming"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4384-6351","authenticated-orcid":false,"given":"Cameron","family":"Moy","sequence":"first","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0009-0008-3242-6969","authenticated-orcid":false,"given":"Jack","family":"Czenszak","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-2130-5092","authenticated-orcid":false,"given":"John M.","family":"Li","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7744-4932","authenticated-orcid":false,"given":"Brianna","family":"Marshall","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8190-5412","authenticated-orcid":false,"given":"Steven","family":"Holtzen","sequence":"additional","affiliation":[{"name":"Northeastern University, Boston, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,6,13]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3674627"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Boris K\u00f6pf Federico Olmedo and Santiago Zanella Beguelin. 2012. Probabilistic Relational Reasoning for Differential Privacy. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/2492061 10.1145\/2492061","DOI":"10.1145\/2492061"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","unstructured":"James Bornholt and Emina Torlak. 2018. Finding Code That Explodes Under Symbolic Evaluation. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/3276519 10.1145\/3276519","DOI":"10.1145\/3276519"},{"key":"e_1_2_2_4_1","volume-title":"Relational Programming in miniKanren: Techniques, Applications, and Implementations. Ph. D. Dissertation","author":"Byrd William E","unstructured":"William E Byrd. 2009. Relational Programming in miniKanren: Techniques, Applications, and Implementations. Ph. D. Dissertation. Indiana University."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","unstructured":"William X Cao Poorva Garg Ryan Tjoa Steven Holtzen Todd Millstein and Guy Van den Broeck. 2023. Scaling Integer Arithmetic in Probabilistic Programs. In Uncertainty in Artificial Intelligence (UAI). https:\/\/doi.org\/10.48550\/arXiv.2307.13837 10.48550\/arXiv.2307.13837","DOI":"10.48550\/arXiv.2307.13837"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","unstructured":"Stephen Chang Alex Knauth and Emina Torlak. 2018. Symbolic Types for Lenient Symbolic Execution. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/3158128 10.1145\/3158128","DOI":"10.1145\/3158128"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","unstructured":"Mark Chavira and Adnan Darwiche. 2008. On Probabilistic Inference by Weighted Model Counting. Artificial Intelligence https:\/\/doi.org\/10.1016\/j.artint.2007.11.002 10.1016\/j.artint.2007.11.002","DOI":"10.1016\/j.artint.2007.11.002"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","unstructured":"David Chiang Colin McDonald and Chung-chieh Shan. 2023. Exact Recursive Probabilistic Programming. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/3586050 10.1145\/3586050","DOI":"10.1145\/3586050"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","unstructured":"Arthur Choi Doga Kisa and Adnan Darwiche. 2013. Compiling Probabilistic Graphical Models Using Sentential Decision Diagrams. In Symbolic and Quantitative Approaches to Reasoning with Uncertainty. https:\/\/doi.org\/10.1007\/978-3-642-39091-3_11 10.1007\/978-3-642-39091-3_11","DOI":"10.1007\/978-3-642-39091-3_11"},{"key":"e_1_2_2_10_1","volume-title":"Cosette: An Automated Prover for SQL. In Conference on Innovative Data Systems Research (CIDR).","author":"Chu Shumo","year":"2017","unstructured":"Shumo Chu, Chenglong Wang, Konstantin Weitz, and Alvin Cheung. 2017. Cosette: An Automated Prover for SQL. In Conference on Innovative Data Systems Research (CIDR)."},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_14"},{"key":"e_1_2_2_12_1","volume-title":"Decomposable Negation Normal Form. In AAAI Conference on Artificial Intelligence (AAAI).","author":"Darwiche Adnan","year":"2002","unstructured":"Adnan Darwiche. 2002. A Compiler for Deterministic, Decomposable Negation Normal Form. In AAAI Conference on Artificial Intelligence (AAAI)."},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5591\/978-1-57735-516-8\/IJCAI11-143"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.989"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","unstructured":"Leonardo De Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). https:\/\/doi.org\/10.1007\/978-3-540-78800-3_24 10.1007\/978-3-540-78800-3_24","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"e_1_2_2_16_1","volume-title":"Problog: A Probabilistic Prolog and Its Application in Link Discovery. In International Joint Conference on Artificial Intelligence (IJCAI).","author":"Raedt Luc De","year":"2007","unstructured":"Luc De Raedt, Angelika Kimmig, and Hannu Toivonen. 2007. Problog: A Probabilistic Prolog and Its Application in Link Discovery. In International Joint Conference on Artificial Intelligence (IJCAI)."},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1017\/S1471068414000076"},{"key":"e_1_2_2_18_1","volume-title":"Reference: Racket","author":"Flatt Matthew","year":"2010","unstructured":"Matthew Flatt and PLT. 2010. Reference: Racket. PLT Design Inc.. https:\/\/racket-lang.org\/tr1\/"},{"key":"e_1_2_2_19_1","volume-title":"The Reasoned Schemer","author":"Friedman Daniel P.","unstructured":"Daniel P. Friedman, William E. Byrd, Oleg Kiselyov, and Jason Hemann. 2018. The Reasoned Schemer. MIT Press."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/215206.215372"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3656412"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192400"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-41528-4_4"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386006"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2338965.2336773"},{"key":"e_1_2_2_26_1","volume-title":"Scheme and Functional Programming Workshop.","author":"Hemann Jason","unstructured":"Jason Hemann and Daniel P. Friedman. 2013. \u03bc Kanren: A Minimal Functional Core for Relational Programming. In Scheme and Functional Programming Workshop."},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.4230\/OASICS.ICLP.2017.14"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","unstructured":"Ralf Hinze and Colin Runciman. 2022. Super-Naturals. Journal of Functional Programming (JFP) https:\/\/doi.org\/10.1017\/s0956796822000028 10.1017\/s0956796822000028","DOI":"10.1017\/s0956796822000028"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428208"},{"key":"e_1_2_2_30_1","unstructured":"Steven Holtzen Matthew Wang John Gouwar Sam Stites and Minsung Cho. 2025. The Rust Decision Diagram Library (RSDD). https:\/\/github.com\/neuppl\/rsdd"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFB0039592"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","unstructured":"Rafael Kiesel and Thomas Eiter. 2023. Knowledge Compilation and More with SharpSAT-TD. In Principles of Knowledge Representation and Reasoning (KR). https:\/\/doi.org\/10.24963\/kr.2023\/40 10.24963\/kr.2023\/40","DOI":"10.24963\/kr.2023\/40"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","unstructured":"Lutz Klinkenberg Christian Blumenthal Mingshuai Chen Darion Haase and Joost-Pieter Katoen. 2024. Exact Bayesian Inference for Loopy Probabilistic Programs using Generating Functions. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/3649844 10.1145\/3649844","DOI":"10.1145\/3649844"},{"key":"e_1_2_2_34_1","volume-title":"The Art of Computer Programming. 4","author":"Knuth Donald E","unstructured":"Donald E Knuth. 2009. The Art of Computer Programming. 4, Addison-Wesley Professional."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.24963\/ijcai.2017\/93"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.15253254"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-30353-1_36"},{"key":"e_1_2_2_38_1","volume-title":"Delayed Sampling and Automatic Rao-Blackwellization of Probabilistic Programs. In International Conference on Artificial Intelligence and Statistics.","author":"Murray Lawrence","year":"2018","unstructured":"Lawrence Murray, Daniel Lund\u00e9n, Jan Kudlicka, David Broman, and Thomas Sch\u00f6n. 2018. Delayed Sampling and Automatic Rao-Blackwellization of Probabilistic Programs. In International Conference on Artificial Intelligence and Statistics."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","unstructured":"Praveen Narayanan Jacques Carette Wren Romano Chung-chieh Shan and Robert Zinkov. 2016. Probabilistic Inference by Program Transformation in Hakaru (System Description). In Functional and Logic Programming (FLOPS). https:\/\/doi.org\/10.1007\/978-3-319-29604-3_5 10.1007\/978-3-319-29604-3_5","DOI":"10.1007\/978-3-319-29604-3_5"},{"key":"e_1_2_2_40_1","volume-title":"Emina Torlak, and Xi Wang.","author":"Nelson Luke","year":"2020","unstructured":"Luke Nelson, Jacob Van Geffen, Emina Torlak, and Xi Wang. 2020. Specification and Verification in the Field: Applying Formal Methods to BPF Just-in-Time Compilers in the Linux Kernel. In Operating Systems Design and Implementation (OSDI)."},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","unstructured":"Raymond Ng and Venkatramanan Siva Subrahmanian. 1992. Probabilistic Logic Programming. Information and Computation https:\/\/doi.org\/10.1016\/0890-5401(92)90061-J 10.1016\/0890-5401(92)90061-J","DOI":"10.1016\/0890-5401(92)90061-J"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/CSF61375.2024.00048"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-49498-1_23"},{"key":"e_1_2_2_44_1","unstructured":"Umut Oztok Arthur Choi and Adnan Darwiche. 2016. Solving PP^ PP-Complete Problems using Knowledge Compilation. In Principles of Knowledge Representation and Reasoning (KR)."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.5555\/2832581.2832687"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1613\/jair.1.11201"},{"key":"e_1_2_2_47_1","volume-title":"Bayesian Networks: A Model of Self-Activated Memory for Evidential Reasoning. In Conference of the Cognitive Science Society.","author":"Pearl Judea","year":"1985","unstructured":"Judea Pearl. 1985. Bayesian Networks: A Model of Self-Activated Memory for Evidential Reasoning. In Conference of the Cognitive Science Society."},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","unstructured":"Stuart Pernsteiner Calvin Loncaric Emina Torlak Zachary Tatlock Xi Wang Michael D. Ernst and Jonathan Jacky. 2016. Investigating Safety of a Radiotherapy Machine Using System Models with Pluggable Checkers. In Computer Aided Verification (CAV). https:\/\/doi.org\/10.1007\/978-3-319-41540-6_2 10.1007\/978-3-319-41540-6_2","DOI":"10.1007\/978-3-319-41540-6_2"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","unstructured":"Phitchaya Mangpo Phothilimthana Aditya Thakur Rastislav Bod\u00edk and Dinakar Dhurjati. 2016. Scaling up Superoptimization. In Architectural Support for Programming Languages and Operating Systems (ASPLOS). https:\/\/doi.org\/10.1145\/2872362.2872387 10.1145\/2872362.2872387","DOI":"10.1145\/2872362.2872387"},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139084673"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","unstructured":"Sorawee Porncharoenwase James Bornholt and Emina Torlak. 2020. Fixing Code That Explodes Under Symbolic Evaluation. In Verification Model Checking and Abstract Interpretation (VMCAI). https:\/\/doi.org\/10.1007\/978-3-030-39322-9_3 10.1007\/978-3-030-39322-9_3","DOI":"10.1007\/978-3-030-39322-9_3"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","unstructured":"Sorawee Porncharoenwase Luke Nelson Xi Wang and Emina Torlak. 2022. A Formal Foundation for Symbolic Evaluation with Merging. In Principles of Programming Languages (POPL). https:\/\/doi.org\/10.1145\/3498709 10.1145\/3498709","DOI":"10.1145\/3498709"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1109\/5.18626"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","unstructured":"Dan Roth. 1996. On the Hardness of Approximate Reasoning. Artificial Intelligence https:\/\/doi.org\/10.1016\/0004-3702(94)00092-1 10.1016\/0004-3702(94)00092-1","DOI":"10.1016\/0004-3702(94)00092-1"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","unstructured":"Colin Runciman. 1989. What About the Natural Numbers? Computer Languages https:\/\/doi.org\/10.1016\/0096-0551(89)90004-0 10.1016\/0096-0551(89)90004-0","DOI":"10.1016\/0096-0551(89)90004-0"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3453483.3454078"},{"key":"e_1_2_2_57_1","volume-title":"AAAI Conference on Artificial Intelligence (AAAI).","author":"Sang Tian","year":"2005","unstructured":"Tian Sang, Paul Beame, and Henry A Kautz. 2005. Performing Bayesian Inference by Weighted Model Counting. In AAAI Conference on Artificial Intelligence (AAAI)."},{"key":"e_1_2_2_58_1","doi-asserted-by":"publisher","unstructured":"Steffen Smolka Praveen Kumar David M. Kahn Nate Foster Justin Hsu Dexter Kozen and Alexandra Silva. 2019. Scalable Verification of Probabilistic Networks. In Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/3314221.3314639 10.1145\/3314221.3314639","DOI":"10.1145\/3314221.3314639"},{"key":"e_1_2_2_59_1","volume-title":"CUDD: CU Decision Diagram Package Release. https:\/\/add-lib.scce.info\/assets\/documents\/cudd-manual.pdf","author":"Somenzi Fabio","year":"1998","unstructured":"Fabio Somenzi. 1998. CUDD: CU Decision Diagram Package Release. https:\/\/add-lib.scce.info\/assets\/documents\/cudd-manual.pdf"},{"key":"e_1_2_2_60_1","doi-asserted-by":"publisher","unstructured":"Zachary Susag Sumit Lahiri Justin Hsu and Subhajit Roy. 2022. Symbolic Execution for Randomized Programs. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/3563344 10.1145\/3563344","DOI":"10.1145\/3563344"},{"key":"e_1_2_2_61_1","doi-asserted-by":"publisher","unstructured":"Emina Torlak and Rastislav Bodik. 2013. Growing Solver-Aided Languages with Rosette. In Onward!. https:\/\/doi.org\/10.1145\/2509578.2509586 10.1145\/2509578.2509586","DOI":"10.1145\/2509578.2509586"},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","unstructured":"Emina Torlak and Rastislav Bod\u00edk. 2014. A Lightweight Symbolic Virtual Machine for Solver-Aided Host Languages. In Programming Language Design and Implementation (PLDI). https:\/\/doi.org\/10.1145\/2594291.2594340 10.1145\/2594291.2594340","DOI":"10.1145\/2594291.2594340"},{"key":"e_1_2_2_63_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-43835-6_23"},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","unstructured":"Konstantin Weitz Doug Woos Emina Torlak Michael D. Ernst Arvind Krishnamurthy and Zachary Tatlock. 2016. Scalable Verification of Border Gateway Protocol Configurations with an SMT Solver. In Object-Oriented Programming Systems Languages and Applications (OOPSLA). https:\/\/doi.org\/10.1145\/2983990.2984012 10.1145\/2983990.2984012","DOI":"10.1145\/2983990.2984012"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729334","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3729334","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,16]],"date-time":"2025-07-16T06:05:36Z","timestamp":1752645936000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3729334"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,10]]},"references-count":64,"journal-issue":{"issue":"PLDI","published-print":{"date-parts":[[2025,6,10]]}},"alternative-id":["10.1145\/3729334"],"URL":"https:\/\/doi.org\/10.1145\/3729334","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,6,10]]},"assertion":[{"value":"2024-11-15","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-06","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-13","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}