{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:44:10Z","timestamp":1780994650908,"version":"3.54.1"},"reference-count":68,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T00:00:00Z","timestamp":1576800000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100003725","name":"National Research Foundation of Korea","doi-asserted-by":"crossref","award":["NRF-2018R1A5A1059921,2017M3C4A7068177"],"award-info":[{"award-number":["NRF-2018R1A5A1059921,2017M3C4A7068177"]}],"id":[{"id":"10.13039\/501100003725","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,1]]},"abstract":"<jats:p>Probabilistic programming is the idea of writing models from statistics and machine learning using program notations and reasoning about these models using generic inference engines. Recently its combination with deep learning has been explored intensely, which led to the development of so called deep probabilistic programming languages, such as Pyro, Edward and ProbTorch. At the core of this development lie inference engines based on stochastic variational inference algorithms. When asked to find information about the posterior distribution of a model written in such a language, these algorithms convert this posterior-inference query into an optimisation problem and solve it approximately by a form of gradient ascent or descent. In this paper, we analyse one of the most fundamental and versatile variational inference algorithms, called score estimator or REINFORCE, using tools from denotational semantics and program analysis. We formally express what this algorithm does on models denoted by programs, and expose implicit assumptions made by the algorithm on the models. The violation of these assumptions may lead to an undefined optimisation objective or the loss of convergence guarantee of the optimisation process. We then describe rules for proving these assumptions, which can be automated by static program analyses. Some of our rules use nontrivial facts from continuous mathematics, and let us replace requirements about integrals in the assumptions, such as integrability of functions defined in terms of programs' denotations, by conditions involving differentiation or boundedness, which are much easier to prove automatically (and manually). Following our general methodology, we have developed a static program analysis for the Pyro programming language that aims at discharging the assumption about what we call model-guide support match. Our analysis is applied to the eight representative model-guide pairs from the Pyro webpage, which include sophisticated neural network models such as AIR. It finds a bug in one of these cases, reveals a non-standard use of an inference engine in another, and shows that the assumptions are met in the remaining six cases.<\/jats:p>","DOI":"10.1145\/3371084","type":"journal-article","created":{"date-parts":[[2019,12,20]],"date-time":"2019-12-20T19:45:25Z","timestamp":1576871125000},"page":"1-33","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":15,"title":["Towards verified stochastic variational inference for probabilistic programs"],"prefix":"10.1145","volume":"4","author":[{"given":"Wonyeol","family":"Lee","sequence":"first","affiliation":[{"name":"KAIST, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hangyeol","family":"Yu","sequence":"additional","affiliation":[{"name":"KAIST, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Xavier","family":"Rival","sequence":"additional","affiliation":[{"name":"Inria, France \/ ENS, France \/ CNRS, France \/ PSL University, France"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Hongseok","family":"Yang","sequence":"additional","affiliation":[{"name":"KAIST, South Korea"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2019,12,20]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"Gray","author":"Bhat Sooraj","year":"2012","unstructured":"Sooraj Bhat , Ashish Agarwal , Richard W. Vuduc , and Alexander G . Gray . 2012 . A type theory for probability density functions. In Principles of Programming Languages (POPL) . 545\u2013556. Sooraj Bhat, Ashish Agarwal, Richard W. Vuduc, and Alexander G. Gray. 2012. A type theory for probability density functions. In Principles of Programming Languages (POPL). 545\u2013556."},{"key":"e_1_2_2_2_1","volume-title":"Russo","author":"Bhat Sooraj","year":"2013","unstructured":"Sooraj Bhat , Johannes Borgstr\u00f6m , Andrew D. Gordon , and Claudio V . Russo . 2013 . Deriving Probability Density Functions from Probabilistic Functional Programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS) . 508\u2013522. Sooraj Bhat, Johannes Borgstr\u00f6m, Andrew D. Gordon, and Claudio V. Russo. 2013. Deriving Probability Density Functions from Probabilistic Functional Programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS). 508\u2013522."},{"key":"e_1_2_2_3_1","first-page":"1","article-title":"Pyro: Deep Universal Probabilistic Programming","volume":"20","author":"Bingham Eli","year":"2019","unstructured":"Eli Bingham , Jonathan P. Chen , Martin Jankowiak , Fritz Obermeyer , Neeraj Pradhan , Theofanis Karaletsos , Rohit Singh , Paul A. Szerlip , Paul Horsfall , and Noah D. Goodman . 2019 . Pyro: Deep Universal Probabilistic Programming . Journal of Machine Learning Research 20 , 28 (2019), 1 \u2013 6 . Eli Bingham, Jonathan P. Chen, Martin Jankowiak, Fritz Obermeyer, Neeraj Pradhan, Theofanis Karaletsos, Rohit Singh, Paul A. Szerlip, Paul Horsfall, and Noah D. Goodman. 2019. Pyro: Deep Universal Probabilistic Programming. Journal of Machine Learning Research 20, 28 (2019), 1\u20136.","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951942"},{"key":"e_1_2_2_5_1","volume-title":"Importance Weighted Autoencoders. In International Conference on Learning Representations (ICLR).","author":"Burda Yuri","year":"2016","unstructured":"Yuri Burda , Roger B. Grosse , and Ruslan Salakhutdinov . 2016 . Importance Weighted Autoencoders. In International Conference on Learning Representations (ICLR). Yuri Burda, Roger B. Grosse, and Ruslan Salakhutdinov. 2016. Importance Weighted Autoencoders. In International Conference on Learning Representations (ICLR)."},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.18637\/jss.v076.i01"},{"key":"e_1_2_2_7_1","volume-title":"Rajamani","author":"Chaganty Arun Tejasvi","year":"2013","unstructured":"Arun Tejasvi Chaganty , Aditya V. Nori , and Sriram K . Rajamani . 2013 . Efficiently Sampling Probabilistic Programs via Program Analysis. In Artificial Intelligence and Statistics (AISTATS) . 153\u2013160. Arun Tejasvi Chaganty, Aditya V. Nori, and Sriram K. Rajamani. 2013. Efficiently Sampling Probabilistic Programs via Program Analysis. In Artificial Intelligence and Statistics (AISTATS). 153\u2013160."},{"key":"e_1_2_2_8_1","doi-asserted-by":"crossref","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Computer Aided Verification (CAV). 511\u2013526.  Aleksandar Chakarov and Sriram Sankaranarayanan. 2013. Probabilistic Program Analysis with Martingales. In Computer Aided Verification (CAV). 511\u2013526.","DOI":"10.1007\/978-3-642-39799-8_34"},{"key":"e_1_2_2_9_1","doi-asserted-by":"crossref","unstructured":"Swarat Chaudhuri Sumit Gulwani and Roberto Lublinerman. 2010. Continuity analysis of programs. In Principles of Programming Languages (POPL). 57\u201370.  Swarat Chaudhuri Sumit Gulwani and Roberto Lublinerman. 2010. Continuity analysis of programs. In Principles of Programming Languages (POPL). 57\u201370.","DOI":"10.1145\/1707801.1706308"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512973"},{"key":"e_1_2_2_11_1","doi-asserted-by":"crossref","unstructured":"Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In Principles of Programming Languages (POPL). 269\u2013282.  Patrick Cousot and Radhia Cousot. 1979. Systematic design of program analysis frameworks. In Principles of Programming Languages (POPL). 269\u2013282.","DOI":"10.1145\/567752.567778"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/2.4.511"},{"key":"e_1_2_2_13_1","volume-title":"Probabilistic Abstract Interpretation. In European Symposium on Programming (ESOP). 169\u2013193","author":"Cousot Patrick","year":"2012","unstructured":"Patrick Cousot and Michael Monerau . 2012 . Probabilistic Abstract Interpretation. In European Symposium on Programming (ESOP). 169\u2013193 . Patrick Cousot and Michael Monerau. 2012. Probabilistic Abstract Interpretation. In European Symposium on Programming (ESOP). 169\u2013193."},{"key":"e_1_2_2_14_1","doi-asserted-by":"crossref","unstructured":"Thomas Ehrhard Christine Tasson and Michele Pagani. 2014. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Principles of Programming Languages (POPL). 309\u2013320.  Thomas Ehrhard Christine Tasson and Michele Pagani. 2014. Probabilistic coherence spaces are fully abstract for probabilistic PCF. In Principles of Programming Languages (POPL). 309\u2013320.","DOI":"10.1145\/2578855.2535865"},{"key":"e_1_2_2_15_1","volume-title":"Hinton","author":"Ali Eslami S. M.","year":"2016","unstructured":"S. M. Ali Eslami , Nicolas Heess , Theophane Weber , Yuval Tassa , David Szepesvari , Koray Kavukcuoglu , and Geoffrey E . Hinton . 2016 . Attend, Infer, Repeat : Fast Scene Understanding with Generative Models. In Neural Information Processing Systems (NIPS) . 3233\u20133241. S. M. Ali Eslami, Nicolas Heess, Theophane Weber, Yuval Tassa, David Szepesvari, Koray Kavukcuoglu, and Geoffrey E. Hinton. 2016. Attend, Infer, Repeat: Fast Scene Understanding with Generative Models. In Neural Information Processing Systems (NIPS). 3233\u20133241."},{"key":"e_1_2_2_16_1","volume-title":"Vechev","author":"Gehr Timon","year":"2016","unstructured":"Timon Gehr , Sasa Misailovic , and Martin T . Vechev . 2016 . PSI : Exact Symbolic Inference for Probabilistic Programs. In Computer Aided Verification (CAV) . 62\u201383. Timon Gehr, Sasa Misailovic, and Martin T. Vechev. 2016. PSI: Exact Symbolic Inference for Probabilistic Programs. In Computer Aided Verification (CAV). 62\u201383."},{"key":"e_1_2_2_17_1","volume-title":"Handbook of Markov Chain Monte Carlo, Steve Brooks, Andrew Gelman, Galin L. Jones, and Xiao-Li Meng (Eds.)","author":"Geyer Charles J.","unstructured":"Charles J. Geyer . 2011. Introduction to Markov Chain Monte Carlo . In Handbook of Markov Chain Monte Carlo, Steve Brooks, Andrew Gelman, Galin L. Jones, and Xiao-Li Meng (Eds.) . Chapman and Hall\/CRC , Chapter 1, 3\u201348. Charles J. Geyer. 2011. Introduction to Markov Chain Monte Carlo. In Handbook of Markov Chain Monte Carlo, Steve Brooks, Andrew Gelman, Galin L. Jones, and Xiao-Li Meng (Eds.). Chapman and Hall\/CRC, Chapter 1, 3\u201348."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/LCOMM.2017.2689770"},{"key":"e_1_2_2_19_1","unstructured":"Noah Goodman Vikash Mansinghka Daniel M Roy Keith Bonawitz and Joshua B Tenenbaum. 2008. Church: a language for generative models. In Uncertainty in Artificial Intelligence (UAI). 220\u2013229.  Noah Goodman Vikash Mansinghka Daniel M Roy Keith Bonawitz and Joshua B Tenenbaum. 2008. Church: a language for generative models. In Uncertainty in Artificial Intelligence (UAI). 220\u2013229."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535850"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/82.4.711"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1093\/biomet\/57.1.97"},{"key":"e_1_2_2_23_1","doi-asserted-by":"crossref","unstructured":"Chris Heunen Ohad Kammar Sam Staton and Hongseok Yang. 2017. A convenient category for higher-order probability theory. In Logic in Computer Science (LICS). 1\u201312.  Chris Heunen Ohad Kammar Sam Staton and Hongseok Yang. 2017. A convenient category for higher-order probability theory. In Logic in Computer Science (LICS). 1\u201312.","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/2567709.2502622"},{"key":"e_1_2_2_25_1","volume-title":"A Provably Correct Sampler for Probabilistic Programs","author":"Hur Chung-Kil","unstructured":"Chung-Kil Hur , Aditya V. Nori , Sriram K. Rajamani , and Selva Samuel . 2015. A Provably Correct Sampler for Probabilistic Programs . In Foundation of Software Technology and Theoretical Computer Science (FSTTCS) . 475\u2013488. Chung-Kil Hur, Aditya V. Nori, Sriram K. Rajamani, and Selva Samuel. 2015. A Provably Correct Sampler for Probabilistic Programs. In Foundation of Software Technology and Theoretical Computer Science (FSTTCS). 475\u2013488."},{"key":"e_1_2_2_26_1","volume-title":"Plotkin","author":"Jones C.","year":"1989","unstructured":"C. Jones and Gordon D . Plotkin . 1989 . A Probabilistic Powerdomain of Evaluations. In Logic in Computer Science (LICS) . 186\u2013195. C. Jones and Gordon D. Plotkin. 1989. A Probabilistic Powerdomain of Evaluations. In Logic in Computer Science (LICS). 186\u2013195."},{"key":"e_1_2_2_27_1","unstructured":"Diederik P. Kingma Danilo J. Rezende Shakir Mohamed and Max Welling. 2014. Semi-supervised Learning with Deep Generative Models. In Neural Information Processing Systems (NIPS). 3581\u20133589.  Diederik P. Kingma Danilo J. Rezende Shakir Mohamed and Max Welling. 2014. Semi-supervised Learning with Deep Generative Models. In Neural Information Processing Systems (NIPS). 3581\u20133589."},{"key":"e_1_2_2_28_1","volume-title":"Auto-Encoding Variational Bayes. In International Conference on Learning Representations (ICLR).","author":"Diederik","unstructured":"Diederik P. Kingma and Max Welling. 2014 . Auto-Encoding Variational Bayes. In International Conference on Learning Representations (ICLR). Diederik P. Kingma and Max Welling. 2014. Auto-Encoding Variational Bayes. In International Conference on Learning Representations (ICLR)."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-47958-3_19"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-5361-0"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_2_32_1","volume-title":"Structured Inference Networks for Nonlinear State Space Models. In AAAI Conference on Artificial Intelligence (AAAI). 2101\u20132109","author":"Krishnan Rahul G.","year":"2017","unstructured":"Rahul G. Krishnan , Uri Shalit , and David Sontag . 2017 . Structured Inference Networks for Nonlinear State Space Models. In AAAI Conference on Artificial Intelligence (AAAI). 2101\u20132109 . Rahul G. Krishnan, Uri Shalit, and David Sontag. 2017. Structured Inference Networks for Nonlinear State Space Models. In AAAI Conference on Artificial Intelligence (AAAI). 2101\u20132109."},{"key":"e_1_2_2_33_1","volume-title":"Blei","author":"Kucukelbir Alp","year":"2015","unstructured":"Alp Kucukelbir , Rajesh Ranganath , Andrew Gelman , and David M . Blei . 2015 . Automatic Variational Inference in Stan. In Neural Information Processing Systems (NIPS) . 568\u2013576. Alp Kucukelbir, Rajesh Ranganath, Andrew Gelman, and David M. Blei. 2015. Automatic Variational Inference in Stan. In Neural Information Processing Systems (NIPS). 568\u2013576."},{"key":"e_1_2_2_34_1","article-title":"Automatic Differentiation Variational Inference","volume":"18","author":"Kucukelbir Alp","year":"2017","unstructured":"Alp Kucukelbir , Dustin Tran , Rajesh Ranganath , Andrew Gelman , and David M. Blei . 2017 . Automatic Differentiation Variational Inference . Journal of Machine Learning Research 18 (2017), 14:1\u201314:45. Alp Kucukelbir, Dustin Tran, Rajesh Ranganath, Andrew Gelman, and David M. Blei. 2017. Automatic Differentiation Variational Inference. Journal of Machine Learning Research 18 (2017), 14:1\u201314:45.","journal-title":"Journal of Machine Learning Research"},{"key":"e_1_2_2_35_1","volume-title":"Atilim Gunes Baydin, and Frank Wood","author":"Le Tuan Anh","year":"2017","unstructured":"Tuan Anh Le , Atilim Gunes Baydin, and Frank Wood . 2017 . Inference Compilation and Universal Probabilistic Programming. In Artificial Intelligence and Statistics (AISTATS) . 1338\u20131348. Tuan Anh Le, Atilim Gunes Baydin, and Frank Wood. 2017. Inference Compilation and Universal Probabilistic Programming. In Artificial Intelligence and Statistics (AISTATS). 1338\u20131348."},{"key":"e_1_2_2_36_1","volume-title":"Towards Verified Stochastic Variational Inference for Probabilistic Programs. arXiv:1907.08827","author":"Lee Wonyeol","year":"2019","unstructured":"Wonyeol Lee , Hangyeol Yu , Xavier Rival , and Hongseok Yang . 2019. Towards Verified Stochastic Variational Inference for Probabilistic Programs. arXiv:1907.08827 ( 2019 ). Wonyeol Lee, Hangyeol Yu, Xavier Rival, and Hongseok Yang. 2019. Towards Verified Stochastic Variational Inference for Probabilistic Programs. arXiv:1907.08827 (2019)."},{"key":"e_1_2_2_37_1","volume-title":"Perov","author":"Mansinghka Vikash K.","year":"2014","unstructured":"Vikash K. Mansinghka , Daniel Selsam , and Yura N . Perov . 2014 . Venture : a higher-order probabilistic programming platform with programmable inference. arXiv:1404.0099 (2014). Vikash K. Mansinghka, Daniel Selsam, and Yura N. Perov. 2014. Venture: a higher-order probabilistic programming platform with programmable inference. arXiv:1404.0099 (2014)."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1063\/1.1699114"},{"key":"e_1_2_2_39_1","unstructured":"T. Minka J.M. Winn J.P. Guiver S. Webster Y. Zaykov B. Yangel A. Spengler and J. Bronskill. 2014. Infer.NET 2.6. Microsoft Research Cambridge. http:\/\/research.microsoft.com\/infernet.  T. Minka J.M. Winn J.P. Guiver S. Webster Y. Zaykov B. Yangel A. Spengler and J. Bronskill. 2014. Infer.NET 2.6. Microsoft Research Cambridge. http:\/\/research.microsoft.com\/infernet."},{"key":"e_1_2_2_40_1","volume-title":"Differentiable Abstract Interpretation for Provably Robust Neural Networks. In International Conference on Machine Learning (ICML). 3575\u20133583","author":"Mirman Matthew","unstructured":"Matthew Mirman , Timon Gehr , and Martin T. Vechev . 2018 . Differentiable Abstract Interpretation for Provably Robust Neural Networks. In International Conference on Machine Learning (ICML). 3575\u20133583 . Matthew Mirman, Timon Gehr, and Martin T. Vechev. 2018. Differentiable Abstract Interpretation for Provably Robust Neural Networks. In International Conference on Machine Learning (ICML). 3575\u20133583."},{"key":"e_1_2_2_41_1","volume-title":"Abstract Interpretation of Probabilistic Semantics. In Static Analysis Symposium (SAS). 322\u2013339","author":"Monniaux David","year":"2000","unstructured":"David Monniaux . 2000 . Abstract Interpretation of Probabilistic Semantics. In Static Analysis Symposium (SAS). 322\u2013339 . David Monniaux. 2000. Abstract Interpretation of Probabilistic Semantics. In Static Analysis Symposium (SAS). 322\u2013339."},{"key":"e_1_2_2_42_1","volume-title":"Backwards Abstract Interpretation of Probabilistic Programs. In European Symposium on Programming (ESOP). 367\u2013382","author":"Monniaux David","year":"2001","unstructured":"David Monniaux . 2001 . Backwards Abstract Interpretation of Probabilistic Programs. In European Symposium on Programming (ESOP). 367\u2013382 . David Monniaux. 2001. Backwards Abstract Interpretation of Probabilistic Programs. In European Symposium on Programming (ESOP). 367\u2013382."},{"key":"e_1_2_2_43_1","volume-title":"On Entropy for Mixtures of Discrete and Continuous Variables. arXiv:cs\/0607075","author":"Nair Chandra","year":"2006","unstructured":"Chandra Nair , Balaji Prabhakar , and Devavrat Shah . 2006. On Entropy for Mixtures of Discrete and Continuous Variables. arXiv:cs\/0607075 ( 2006 ). Chandra Nair, Balaji Prabhakar, and Devavrat Shah. 2006. On Entropy for Mixtures of Discrete and Continuous Variables. arXiv:cs\/0607075 (2006)."},{"key":"e_1_2_2_44_1","doi-asserted-by":"crossref","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). 62\u201379.  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). 62\u201379.","DOI":"10.1007\/978-3-319-29604-3_5"},{"key":"e_1_2_2_45_1","volume-title":"Hinton","author":"Neal Radford M.","year":"1998","unstructured":"Radford M. Neal and Geoffrey E . Hinton . 1998 . A View of the Em Algorithm that Justifies Incremental, Sparse, and other Variants. In Learning in Graphical Models . 355\u2013368. Radford M. Neal and Geoffrey E. Hinton. 1998. A View of the Em Algorithm that Justifies Incremental, Sparse, and other Variants. In Learning in Graphical Models. 355\u2013368."},{"key":"e_1_2_2_46_1","volume-title":"AAAI Conference on Artificial Intelligence (AAAI). 2476\u20132482","author":"Nori Aditya V.","year":"2014","unstructured":"Aditya V. Nori , Chung-Kil Hur , Sriram K. Rajamani , and Selva Samuel . 2014 . R2: An Efficient MCMC Sampler for Probabilistic Programs . In AAAI Conference on Artificial Intelligence (AAAI). 2476\u20132482 . Aditya V. Nori, Chung-Kil Hur, Sriram K. Rajamani, and Selva Samuel. 2014. R2: An Efficient MCMC Sampler for Probabilistic Programs. In AAAI Conference on Artificial Intelligence (AAAI). 2476\u20132482."},{"key":"e_1_2_2_47_1","volume-title":"Variational Bayesian Inference with Stochastic Search. In International Conference on Machine Learning (ICML). 1363\u20131370","author":"Paisley John William","unstructured":"John William Paisley , David M. Blei , and Michael I. Jordan . 2012 . Variational Bayesian Inference with Stochastic Search. In International Conference on Machine Learning (ICML). 1363\u20131370 . John William Paisley, David M. Blei, and Michael I. Jordan. 2012. Variational Bayesian Inference with Stochastic Search. In International Conference on Machine Learning (ICML). 1363\u20131370."},{"key":"e_1_2_2_48_1","volume-title":"Blei","author":"Ranganath Rajesh","year":"2014","unstructured":"Rajesh Ranganath , Sean Gerrish , and David M . Blei . 2014 . Black Box Variational Inference. In Artificial Intelligence and Statistics (AISTATS) . 814\u2013822. Rajesh Ranganath, Sean Gerrish, and David M. Blei. 2014. Black Box Variational Inference. In Artificial Intelligence and Statistics (AISTATS). 814\u2013822."},{"key":"e_1_2_2_49_1","unstructured":"Rajesh Ranganath Linpeng Tang Laurent Charlin and David Blei. 2015. Deep Exponential Families. In Artificial Intelligence and Statistics (AISTATS). 762\u2013771.  Rajesh Ranganath Linpeng Tang Laurent Charlin and David Blei. 2015. Deep Exponential Families. In Artificial Intelligence and Statistics (AISTATS). 762\u2013771."},{"key":"e_1_2_2_50_1","volume-title":"POPL","author":"Scibior Adam","year":"2018","unstructured":"Adam Scibior , Ohad Kammar , Matthijs V\u00e1k\u00e1r , Sam Staton , Hongseok Yang , Yufei Cai , Klaus Ostermann , Sean K. Moss , Chris Heunen , and Zoubin Ghahramani . 2018. Denotational validation of higher-order Bayesian inference. PACMPL 2 , POPL ( 2018 ), 60:1\u201360:29. Adam Scibior, Ohad Kammar, Matthijs V\u00e1k\u00e1r, Sam Staton, Hongseok Yang, Yufei Cai, Klaus Ostermann, Sean K. Moss, Chris Heunen, and Zoubin Ghahramani. 2018. Denotational validation of higher-order Bayesian inference. PACMPL 2, POPL (2018), 60:1\u201360:29."},{"key":"e_1_2_2_51_1","unstructured":"N. Siddharth Brooks Paige Jan-Willem van de Meent Alban Desmaison Noah D. Goodman Pushmeet Kohli Frank Wood and Philip Torr. 2017. Learning Disentangled Representations with Semi-Supervised Deep Generative Models. In Neural Information Processing Systems (NIPS). 5927\u20135937.  N. Siddharth Brooks Paige Jan-Willem van de Meent Alban Desmaison Noah D. Goodman Pushmeet Kohli Frank Wood and Philip Torr. 2017. Learning Disentangled Representations with Semi-Supervised Deep Generative Models. In Neural Information Processing Systems (NIPS). 5927\u20135937."},{"key":"e_1_2_2_52_1","doi-asserted-by":"crossref","unstructured":"Steffen Smolka Praveen Kumar Nate Foster Dexter Kozen and Alexandra Silva. 2017. Cantor meets scott: semantic foundations for probabilistic networks. In Principles of Programming Languages (POPL). 557\u2013571.  Steffen Smolka Praveen Kumar Nate Foster Dexter Kozen and Alexandra Silva. 2017. Cantor meets scott: semantic foundations for probabilistic networks. In Principles of Programming Languages (POPL). 557\u2013571.","DOI":"10.1145\/3093333.3009843"},{"key":"e_1_2_2_53_1","volume-title":"Autoencoding Variational Inference For Topic Models. In International Conference on Learning Representations (ICLR).","author":"Srivastava Akash","unstructured":"Akash Srivastava and Charles A. Sutton . 2017 . Autoencoding Variational Inference For Topic Models. In International Conference on Learning Representations (ICLR). Akash Srivastava and Charles A. Sutton. 2017. Autoencoding Variational Inference For Topic Models. In International Conference on Learning Representations (ICLR)."},{"key":"e_1_2_2_54_1","volume-title":"Commutative Semantics for Probabilistic Programming. In European Symposium on Programming (ESOP). 855\u2013879","author":"Staton Sam","year":"2017","unstructured":"Sam Staton . 2017 . Commutative Semantics for Probabilistic Programming. In European Symposium on Programming (ESOP). 855\u2013879 . Sam Staton. 2017. Commutative Semantics for Probabilistic Programming. In European Symposium on Programming (ESOP). 855\u2013879."},{"key":"e_1_2_2_55_1","doi-asserted-by":"crossref","unstructured":"Sam Staton Hongseok Yang Frank D. Wood Chris Heunen and Ohad Kammar. 2016. Semantics for probabilistic programming: higher-order functions continuous distributions and soft constraints. In Logic in Computer Science (LICS). 525\u2013534.  Sam Staton Hongseok Yang Frank D. Wood Chris Heunen and Ohad Kammar. 2016. Semantics for probabilistic programming: higher-order functions continuous distributions and soft constraints. In Logic in Computer Science (LICS). 525\u2013534.","DOI":"10.1145\/2933575.2935313"},{"key":"e_1_2_2_56_1","volume-title":"Running Probabilistic Programs Backwards. In European Symposium on Programming (ESOP). 53\u201379","author":"Toronto Neil","year":"2015","unstructured":"Neil Toronto , Jay McCarthy , and David Van Horn . 2015 . Running Probabilistic Programs Backwards. In European Symposium on Programming (ESOP). 53\u201379 . Neil Toronto, Jay McCarthy, and David Van Horn. 2015. Running Probabilistic Programs Backwards. In European Symposium on Programming (ESOP). 53\u201379."},{"key":"e_1_2_2_57_1","unstructured":"Dustin Tran Matthew D. Hoffman Dave Moore Christopher Suter Srinivas Vasudevan and Alexey Radul. 2018. Simple Distributed and Accelerated Probabilistic Programming. In Neural Information Processing Systems (NeurIPS). 7609\u20137620.  Dustin Tran Matthew D. Hoffman Dave Moore Christopher Suter Srinivas Vasudevan and Alexey Radul. 2018. Simple Distributed and Accelerated Probabilistic Programming. In Neural Information Processing Systems (NeurIPS). 7609\u20137620."},{"key":"e_1_2_2_58_1","volume-title":"Blei","author":"Tran Dustin","year":"2016","unstructured":"Dustin Tran , Alp Kucukelbir , Adji B. Dieng , Maja R. Rudolph , Dawen Liang , and David M . Blei . 2016 . Edward : A library for probabilistic modeling, inference, and criticism. arXiv:1610.09787 (2016). Dustin Tran, Alp Kucukelbir, Adji B. Dieng, Maja R. Rudolph, Dawen Liang, and David M. Blei. 2016. Edward: A library for probabilistic modeling, inference, and criticism. arXiv:1610.09787 (2016)."},{"key":"e_1_2_2_59_1","unstructured":"Uber AI Labs. 2019a. Pyro examples. http:\/\/pyro.ai\/examples\/ . Version used: April 1 2019.  Uber AI Labs. 2019a. Pyro examples. http:\/\/pyro.ai\/examples\/ . Version used: April 1 2019."},{"key":"e_1_2_2_60_1","volume-title":"Pyro regression test suite. https:\/\/github.com\/pyro- ppl\/pyro\/blob\/dev\/tests\/infer\/test_valid_models.py . Version used","author":"Labs Uber AI","year":"2019","unstructured":"Uber AI Labs . 2019b. Pyro regression test suite. https:\/\/github.com\/pyro- ppl\/pyro\/blob\/dev\/tests\/infer\/test_valid_models.py . Version used : March 1, 2019 . Uber AI Labs. 2019b. Pyro regression test suite. https:\/\/github.com\/pyro- ppl\/pyro\/blob\/dev\/tests\/infer\/test_valid_models.py . Version used: March 1, 2019."},{"key":"e_1_2_2_61_1","volume-title":"POPL","author":"V\u00e1k\u00e1r Matthijs","year":"2019","unstructured":"Matthijs V\u00e1k\u00e1r , Ohad Kammar , and Sam Staton . 2019. A domain theory for statistical probabilistic programming. PACMPL 3 , POPL ( 2019 ), 36:1\u201336:29. Matthijs V\u00e1k\u00e1r, Ohad Kammar, and Sam Staton. 2019. A domain theory for statistical probabilistic programming. PACMPL 3, POPL (2019), 36:1\u201336:29."},{"key":"e_1_2_2_62_1","volume-title":"Wood","author":"van de Meent Jan-Willem","year":"2016","unstructured":"Jan-Willem van de Meent , Brooks Paige , David Tolpin , and Frank D . Wood . 2016 . Black-Box Policy Search with Probabilistic Programs. In Artificial Intelligence and Statistics (AISTATS) . 1195\u20131204. Jan-Willem van de Meent, Brooks Paige, David Tolpin, and Frank D. Wood. 2016. Black-Box Policy Search with Probabilistic Programs. In Artificial Intelligence and Statistics (AISTATS). 1195\u20131204."},{"key":"e_1_2_2_63_1","volume-title":"Reps","author":"Wang Di","year":"2018","unstructured":"Di Wang , Jan Hoffmann , and Thomas W . Reps . 2018 . PMAF: an algebraic framework for static analysis of probabilistic programs. In Programming Language Design and Implementation (PLDI) . 513\u2013528. Di Wang, Jan Hoffmann, and Thomas W. Reps. 2018. PMAF: an algebraic framework for static analysis of probabilistic programs. In Programming Language Design and Implementation (PLDI). 513\u2013528."},{"key":"e_1_2_2_64_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00992696"},{"key":"e_1_2_2_65_1","volume-title":"Automated Variational Inference in Probabilistic Programming. arXiv:1301.1299","author":"Wingate David","year":"2013","unstructured":"David Wingate and Theophane Weber . 2013. Automated Variational Inference in Probabilistic Programming. arXiv:1301.1299 ( 2013 ). David Wingate and Theophane Weber. 2013. Automated Variational Inference in Probabilistic Programming. arXiv:1301.1299 (2013)."},{"key":"e_1_2_2_66_1","volume-title":"Jan Willem van de Meent, and Vikash Mansinghka","author":"Wood Frank","year":"2014","unstructured":"Frank Wood , Jan Willem van de Meent, and Vikash Mansinghka . 2014 . A New Approach to Probabilistic Programming Inference. In Artificial Intelligence and Statistics (AISTATS) . 1024\u20131032. Frank Wood, Jan Willem van de Meent, and Vikash Mansinghka. 2014. A New Approach to Probabilistic Programming Inference. In Artificial Intelligence and Statistics (AISTATS). 1024\u20131032."},{"key":"e_1_2_2_67_1","volume-title":"Discrete-Continuous Mixtures in Probabilistic Programming: Generalized Semantics and Inference Algorithms. In International Conference on Machine Learning (ICML). 5339\u20135348","author":"Wu Yi","unstructured":"Yi Wu , Siddharth Srivastava , Nicholas Hay , Simon Du , and Stuart J. Russell . 2018 . Discrete-Continuous Mixtures in Probabilistic Programming: Generalized Semantics and Inference Algorithms. In International Conference on Machine Learning (ICML). 5339\u20135348 . Yi Wu, Siddharth Srivastava, Nicholas Hay, Simon Du, and Stuart J. Russell. 2018. Discrete-Continuous Mixtures in Probabilistic Programming: Generalized Semantics and Inference Algorithms. In International Conference on Machine Learning (ICML). 5339\u20135348."},{"key":"e_1_2_2_68_1","unstructured":"Hongseok Yang. 2019. Implementing Inference Algorithms for Probabilistic Programs. https:\/\/github.com\/hongseok- yang\/ probprog19\/blob\/master\/Lectures\/Lecture6\/Note6.pdf . Lecture Note of the 2019 Course on Probabilistic Programming at KAIST.  Hongseok Yang. 2019. Implementing Inference Algorithms for Probabilistic Programs. https:\/\/github.com\/hongseok- yang\/ probprog19\/blob\/master\/Lectures\/Lecture6\/Note6.pdf . Lecture Note of the 2019 Course on Probabilistic Programming at KAIST."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371084","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3371084","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T19:05:43Z","timestamp":1750273543000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3371084"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,12,20]]},"references-count":68,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2020,1]]}},"alternative-id":["10.1145\/3371084"],"URL":"https:\/\/doi.org\/10.1145\/3371084","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,12,20]]},"assertion":[{"value":"2019-12-20","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}