{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:14:53Z","timestamp":1767928493105,"version":"3.49.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2019,1,2]],"date-time":"2019-01-02T00:00:00Z","timestamp":1546387200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2019,1,2]]},"abstract":"<jats:p>\n            Probabilistic programming provides a convenient\n            <jats:italic>lingua franca<\/jats:italic>\n            for writing succinct and rigorous descriptions of probabilistic models and inference tasks. Several probabilistic programming languages, including Anglican, Church or Hakaru, derive their expressiveness from a powerful combination of continuous distributions, conditioning, and higher-order functions. Although very important for practical applications, these features raise fundamental challenges for program semantics and verification. Several recent works offer promising answers to these challenges, but their primary focus is on foundational semantics issues.\n          <\/jats:p>\n          <jats:p>In this paper, we take a step further by developing a suite of logics, collectively named PPV for proving properties of programs written in an expressive probabilistic higher-order language with continuous sampling operations and primitives for conditioning distributions. Our logics mimic the comfortable reasoning style of informal proofs using carefully selected axiomatizations of key results from probability theory. The versatility of our logics is illustrated through the formal verification of several intricate examples from statistics, probabilistic inference, and machine learning. We further show expressiveness by giving sound embeddings of existing logics. In particular, we do this in a parametric way by showing how the semantics idea of (unary and relational) \u22a4\u22a4-lifting can be internalized in our logics. The soundness of PPV follows by interpreting programs and assertions in quasi-Borel spaces (QBS), a recently proposed variant of Borel spaces with a good structure for interpreting higher order probabilistic programs.<\/jats:p>","DOI":"10.1145\/3290351","type":"journal-article","created":{"date-parts":[[2019,1,4]],"date-time":"2019-01-04T13:33:51Z","timestamp":1546608831000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":19,"title":["Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization"],"prefix":"10.1145","volume":"3","author":[{"given":"Tetsuya","family":"Sato","sequence":"first","affiliation":[{"name":"SUNY Buffalo, USA"}]},{"given":"Alejandro","family":"Aguirre","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[{"name":"SUNY Buffalo, USA"}]},{"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}]},{"given":"Justin","family":"Hsu","sequence":"additional","affiliation":[{"name":"University of Wisconsin-Madison, USA"}]}],"member":"320","published-online":{"date-parts":[[2019,1,2]]},"reference":[{"key":"e_1_2_2_1_1","volume-title":"ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. 214\u2013241","author":"Aguirre Alejandro","year":"2018","unstructured":"Alejandro Aguirre , Gilles Barthe , Lars Birkedal , Ales Bizjak , Marco Gaboardi , and Deepak Garg . 2018 . Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In Programming Languages and Systems - 27th European Symposium on Programming , ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. 214\u2013241 . Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Ales Bizjak, Marco Gaboardi, and Deepak Garg. 2018. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. In Programming Languages and Systems - 27th European Symposium on Programming, ESOP 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings. 214\u2013241."},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110265"},{"key":"e_1_2_2_3_1","volume-title":"Foundations of Software Science and Computation Structures, Bart Jacobs and Christof L\u00f6ding (Eds.)","author":"Amtoft Torben","unstructured":"Torben Amtoft and Anindya Banerjee . 2016. A Theory of Slicing for Probabilistic Control Flow Graphs . In Foundations of Software Science and Computation Structures, Bart Jacobs and Christof L\u00f6ding (Eds.) . Springer Berlin Heidelberg , Berlin, Heidelberg , 180\u2013196. Torben Amtoft and Anindya Banerjee. 2016. A Theory of Slicing for Probabilistic Control Flow Graphs. In Foundations of Software Science and Computation Structures, Bart Jacobs and Christof L\u00f6ding (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg, 180\u2013196."},{"key":"e_1_2_2_4_1","volume-title":"Littman","author":"Asadi Kavosh","year":"2018","unstructured":"Kavosh Asadi , Evan Cater , Dipendra Misra , and Michael L . Littman . 2018 . Equivalence Between Wasserstein and Value-Aware Model-based Reinforcement Learning. ArXiv e-prints (June 2018). arXiv: cs.LG\/1806.01265 Kavosh Asadi, Evan Cater, Dipendra Misra, and Michael L. Littman. 2018. Equivalence Between Wasserstein and Value-Aware Model-based Reinforcement Learning. ArXiv e-prints (June 2018). arXiv: cs.LG\/1806.01265"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2007.09.002"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1215\/ijm\/1255631584"},{"key":"e_1_2_2_7_1","volume-title":"A formally verified proof of the Central Limit Theorem. CoRR abs\/1405.7012","author":"Avigad Jeremy","year":"2014","unstructured":"Jeremy Avigad , Johannes H\u00f6lzl , and Luke Serafin . 2014. A formally verified proof of the Central Limit Theorem. CoRR abs\/1405.7012 ( 2014 ). http:\/\/arxiv.org\/abs\/1405.7012 Jeremy Avigad, Johannes H\u00f6lzl, and Luke Serafin. 2014. A formally verified proof of the Central Limit Theorem. CoRR abs\/1405.7012 (2014). http:\/\/arxiv.org\/abs\/1405.7012"},{"key":"e_1_2_2_8_1","volume-title":"An AssertionBased Program Logic for Probabilistic Programs","author":"Barthe Gilles","unstructured":"Gilles Barthe , Thomas Espitau , Marco Gaboardi , Benjamin Gr\u00e9goire , Justin Hsu , and Pierre-Yves Strub . 2018. An AssertionBased Program Logic for Probabilistic Programs . In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing , Cham , 117\u2013144. Gilles Barthe, Thomas Espitau, Marco Gaboardi, Benjamin Gr\u00e9goire, Justin Hsu, and Pierre-Yves Strub. 2018. An AssertionBased Program Logic for Probabilistic Programs. In Programming Languages and Systems, Amal Ahmed (Ed.). Springer International Publishing, Cham, 117\u2013144."},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2976749.2978371"},{"key":"e_1_2_2_10_1","volume-title":"43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016","author":"Barthe Gilles","year":"2016","unstructured":"Gilles Barthe , Marco Gaboardi , Benjamin Gr\u00e9goire , Justin Hsu , and Pierre-Yves Strub . 2016 b. A Program Logic for Union Bounds. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016 , July 11-15, 2016, Rome, Italy. 107:1\u2013107:15. Gilles Barthe, Marco Gaboardi, Benjamin Gr\u00e9goire, Justin Hsu, and Pierre-Yves Strub. 2016b. A Program Logic for Union Bounds. In 43rd International Colloquium on Automata, Languages, and Programming, ICALP 2016, July 11-15, 2016, Rome, Italy. 107:1\u2013107:15."},{"key":"e_1_2_2_11_1","volume-title":"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. 77\u201396","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. 77\u201396 . 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. 77\u201396."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951942"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209187"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.02.040"},{"key":"e_1_2_2_15_1","volume-title":"The sample size required in importance sampling. Ann. Appl. Probab. 28, 2 (04","author":"Chatterjee Sourav","year":"2018","unstructured":"Sourav Chatterjee and Persi Diaconis . 2018. The sample size required in importance sampling. Ann. Appl. Probab. 28, 2 (04 2018 ), 1099\u20131135. Sourav Chatterjee and Persi Diaconis. 2018. The sample size required in importance sampling. Ann. Appl. Probab. 28, 2 (04 2018), 1099\u20131135."},{"key":"e_1_2_2_17_1","volume-title":"Bayesian machine learning via category theory. ArXiv e-prints (Dec","author":"Kirk Culbertson","year":"2013","unstructured":"Jared. Culbertson and Kirk . Sturtz. 2013. Bayesian machine learning via category theory. ArXiv e-prints (Dec . 2013 ). arXiv: math.CT\/1312.1445 Jared. Culbertson and Kirk. Sturtz. 2013. Bayesian machine learning via category theory. ArXiv e-prints (Dec. 2013). arXiv: math.CT\/1312.1445"},{"key":"e_1_2_2_18_1","volume-title":"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. 368\u2013392","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. 368\u2013392 . 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. 368\u2013392."},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158147"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535865"},{"key":"e_1_2_2_22_1","volume-title":"Categorical Aspects of Topology and Analysis","author":"Giry Mich\u00e8le","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 . Springer Berlin Heidelberg , 68\u201385. 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. Springer Berlin Heidelberg, 68\u201385."},{"key":"e_1_2_2_23_1","volume-title":"UAI 2008, Proceedings of the 24th Conference in Uncertainty in Artificial Intelligence","author":"Goodman Noah D.","year":"2008","unstructured":"Noah D. Goodman , Vikash K. Mansinghka , Daniel M. Roy , Keith Bonawitz , and Joshua B. Tenenbaum . 2008. Church: a language for generative models . In UAI 2008, Proceedings of the 24th Conference in Uncertainty in Artificial Intelligence , Helsinki, Finland , July 9-12, 2008 . 220\u2013229. https:\/\/dslpitt.org\/uai\/displayArticleDetails.jsp?mmnu=1&amp;smnu=2&amp;article_ id=1346&amp;proceeding_id=24 Noah D. Goodman, Vikash K. Mansinghka, Daniel M. Roy, Keith Bonawitz, and Joshua B. Tenenbaum. 2008. Church: a language for generative models. In UAI 2008, Proceedings of the 24th Conference in Uncertainty in Artificial Intelligence, Helsinki, Finland, July 9-12, 2008. 220\u2013229. https:\/\/dslpitt.org\/uai\/displayArticleDetails.jsp?mmnu=1&amp;smnu=2&amp;article_ id=1346&amp;proceeding_id=24"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2014.10.010"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40196-1_17"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005137"},{"key":"e_1_2_2_27_1","unstructured":"Johannes H\u00f6lzl. 2016. Markov chains and Markov decision processes in Isabelle\/HOL. (2016). http:\/\/home.in.tum.de\/~hoelzl\/ mdptheory\/hoelzl2016markov- draft.pdf  Johannes H\u00f6lzl. 2016. Markov chains and Markov decision processes in Isabelle\/HOL. (2016). http:\/\/home.in.tum.de\/~hoelzl\/ mdptheory\/hoelzl2016markov- draft.pdf"},{"key":"e_1_2_2_28_1","volume-title":"Three","author":"H\u00f6lzl Johannes","year":"2011","unstructured":"Johannes H\u00f6lzl and Armin Heller . 2011. Three Chapters of Measure Theory in Isabelle\/HOL. In Interactive Theorem Proving, ITP 2011 (Lecture Notes in Computer Science), Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk (Eds.), Vol. 6898 . Springer , 135\u2013151. Johannes H\u00f6lzl and Armin Heller. 2011. Three Chapters of Measure Theory in Isabelle\/HOL. In Interactive Theorem Proving, ITP 2011 (Lecture Notes in Computer Science), Marko C. J. D. van Eekelen, Herman Geuvers, Julien Schmaltz, and Freek Wiedijk (Eds.), Vol. 6898. Springer, 135\u2013151."},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.08.005"},{"key":"e_1_2_2_31_1","volume-title":"Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland","author":"Jacobs Bart","unstructured":"Bart Jacobs . 1999. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland , Amsterdam . Bart Jacobs. 1999. Categorical Logic and Type Theory. Number 141 in Studies in Logic and the Foundations of Mathematics. North Holland, Amsterdam."},{"key":"e_1_2_2_32_1","volume-title":"International Conference on Typed Lambda Calculi and Applications, TLCA \u201993","author":"Jacobs Bart","year":"1993","unstructured":"Bart Jacobs and Thomas F. Melham . 1993. Translating Dependent Type Theory into Higher Order Logic. In Typed Lambda Calculi and Applications , International Conference on Typed Lambda Calculi and Applications, TLCA \u201993 , Utrecht, The Netherlands , March 16-18, 1993 , Proceedings. 209\u2013229. Bart Jacobs and Thomas F. Melham. 1993. Translating Dependent Type Theory into Higher Order Logic. In Typed Lambda Calculi and Applications, International Conference on Typed Lambda Calculi and Applications, TLCA \u201993, Utrecht, The Netherlands, March 16-18, 1993, Proceedings. 209\u2013229."},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/77350.77370"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80216-6"},{"key":"e_1_2_2_35_1","doi-asserted-by":"crossref","unstructured":"Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. arXiv: cs.LO\/1601.01001  Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Federico Olmedo. 2016. Weakest Precondition Reasoning for Expected Run-Times of Probabilistic Programs. arXiv: cs.LO\/1601.01001","DOI":"10.1007\/978-3-662-49498-1_15"},{"key":"e_1_2_2_36_1","volume-title":"Morgan","author":"Katoen Joost-Pieter","year":"2010","unstructured":"Joost-Pieter Katoen , Annabelle McIver , Larissa Meinicke , and Carroll C . Morgan . 2010 . Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods . 390\u2013406. Joost-Pieter Katoen, Annabelle McIver, Larissa Meinicke, and Carroll C. Morgan. 2010. Linear-Invariant Generation for Probabilistic Programs: Automated Support for Proof-Based Methods. 390\u2013406."},{"key":"e_1_2_2_37_1","volume-title":"Proc. in Informatics (LIPIcs))","volume":"35","author":"Tetsuya Sato Katsumata","year":"2015","unstructured":"Shin-ya Katsumata and Tetsuya Sato . 2015 . Codensity Liftings of Monads. In Conference on Algebra and Coalgebra in Computer Science (CALCO 2015) (Leibniz Intern . Proc. in Informatics (LIPIcs)) , Vol. 35 . Schloss Dagstuhl, 156\u2013170. Shin-ya Katsumata and Tetsuya Sato. 2015. Codensity Liftings of Monads. In Conference on Algebra and Coalgebra in Computer Science (CALCO 2015) (Leibniz Intern. Proc. in Informatics (LIPIcs)), Vol. 35. Schloss Dagstuhl, 156\u2013170."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535846"},{"key":"e_1_2_2_39_1","volume-title":"Plotkin","author":"Keimel Klaus","year":"2017","unstructured":"Klaus Keimel and Gordon D . Plotkin . 2017 . Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science 13, 1 (2017). Klaus Keimel and Gordon D. Plotkin. 2017. Mixed powerdomains for probability and nondeterminism. Logical Methods in Computer Science 13, 1 (2017)."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(81)90036-2"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_2_42_1","doi-asserted-by":"crossref","unstructured":"A. McIver and C. Morgan. 2005. Abstraction Refinement and Proof for Probabilistic Systems. Springer.   A. McIver and C. Morgan. 2005. Abstraction Refinement and Proof for Probabilistic Systems. Springer.","DOI":"10.1145\/1059816.1059824"},{"key":"e_1_2_2_43_1","volume-title":"Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday. 185\u2013202.","author":"Mislove Michael W.","unstructured":"Michael W. Mislove . 2017. Discrete Random Variables Over Domains , Revisited. In Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday. 185\u2013202. Michael W. Mislove. 2017. Discrete Random Variables Over Domains, Revisited. In Concurrency, Security, and Puzzles - Essays Dedicated to Andrew William Roscoe on the Occasion of His 60th Birthday. 185\u2013202."},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_2_45_1","volume-title":"FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings. 62\u201379","author":"Narayanan Praveen","year":"2016","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 - 13th International Symposium , FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings. 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 - 13th International Symposium, FLOPS 2016, Kochi, Japan, March 4-6, 2016, Proceedings. 62\u201379."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80602-4"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"e_1_2_2_49_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.021"},{"key":"e_1_2_2_50_1","volume-title":"17th International Conference, (TPHOL) 2004 (Lecture Notes in Computer Science), Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan (Eds.)","volume":"3223","author":"Richter Stefan","year":"2004","unstructured":"Stefan Richter . 2004 . Formalizing Integration Theory with an Application to Probabilistic Algorithms. In Theorem Proving in Higher Order Logics , 17th International Conference, (TPHOL) 2004 (Lecture Notes in Computer Science), Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan (Eds.) , Vol. 3223 . Springer, 271\u2013286. Stefan Richter. 2004. Formalizing Integration Theory with an Application to Probabilistic Algorithms. In Theorem Proving in Higher Order Logics, 17th International Conference, (TPHOL) 2004 (Lecture Notes in Computer Science), Konrad Slind, Annette Bunker, and Ganesh Gopalakrishnan (Eds.), Vol. 3223. Springer, 271\u2013286."},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(80)90003-1"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jpaa.2017.11.004"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158148"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009852"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54434-1_32"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2009.01.002"},{"key":"e_1_2_2_57_1","volume-title":"Probabilistic Event Structures and Domains. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings. 481\u2013496","author":"Varacca Daniele","year":"2004","unstructured":"Daniele Varacca , Hagen V\u00f6lzer , and Glynn Winskel . 2004 . Probabilistic Event Structures and Domains. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings. 481\u2013496 . Daniele Varacca, Hagen V\u00f6lzer, and Glynn Winskel. 2004. Probabilistic Event Structures and Domains. In CONCUR 2004 - Concurrency Theory, 15th International Conference, London, UK, August 31 - September 3, 2004, Proceedings. 481\u2013496."},{"key":"e_1_2_2_58_1","volume-title":"Proceedings of the Seventeenth International Conference on Artificial Intelligence and Statistics, AISTATS 2014","author":"Wood Frank D.","year":"2014","unstructured":"Frank D. Wood , Jan-Willem van de Meent, and Vikash Mansinghka. 2014. A New Approach to Probabilistic Programming Inference . In Proceedings of the Seventeenth International Conference on Artificial Intelligence and Statistics, AISTATS 2014 , Reykjavik, Iceland , April 22-25, 2014 . 1024\u20131032. http:\/\/jmlr.org\/proceedings\/papers\/v33\/wood14.html Frank D. Wood, Jan-Willem van de Meent, and Vikash Mansinghka. 2014. A New Approach to Probabilistic Programming Inference. In Proceedings of the Seventeenth International Conference on Artificial Intelligence and Statistics, AISTATS 2014, Reykjavik, Iceland, April 22-25, 2014. 1024\u20131032. http:\/\/jmlr.org\/proceedings\/papers\/v33\/wood14.html"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290351","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3290351","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T00:58:04Z","timestamp":1750208284000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3290351"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,1,2]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2019,1,2]]}},"alternative-id":["10.1145\/3290351"],"URL":"https:\/\/doi.org\/10.1145\/3290351","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,1,2]]},"assertion":[{"value":"2019-01-02","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}