{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:28:54Z","timestamp":1784255334911,"version":"3.55.0"},"reference-count":53,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2024,1,2]],"date-time":"2024-01-02T00:00:00Z","timestamp":1704153600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000781","name":"European Research Council","doi-asserted-by":"publisher","award":["ARTIST 101002685"],"award-info":[{"award-number":["ARTIST 101002685"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001821","name":"Vienna Science and Technology Fund","doi-asserted-by":"publisher","award":["10.47379\/ICT19018"],"award-info":[{"award-number":["10.47379\/ICT19018"]}],"id":[{"id":"10.13039\/501100001821","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":[[2024,1,2]]},"abstract":"<jats:p>\n            We show that computing the strongest polynomial invariant for single-path loops with polynomial assignments is at least as hard as the\n            <jats:xref ref-type=\"fig\">\n              <jats:sc>Skolem<\/jats:sc>\n            <\/jats:xref>\n            problem, a famous problem whose decidability has been open for almost a century. While the strongest polynomial invariants are computable for\n            <jats:italic toggle=\"yes\">affine loops<\/jats:italic>\n            , for polynomial loops the problem remained wide open. As an intermediate result of independent interest, we prove that reachability for discrete polynomial dynamical systems is\n            <jats:xref ref-type=\"fig\">\n              <jats:sc>Skolem<\/jats:sc>\n            <\/jats:xref>\n            -hard as well. Furthermore, we generalize the notion of invariant ideals and introduce\n            <jats:italic toggle=\"yes\">moment invariant ideals<\/jats:italic>\n            for probabilistic programs. With this tool, we further show that the strongest polynomial moment invariant is (i) uncomputable, for probabilistic loops with branching statements, and (ii)\n            <jats:xref ref-type=\"fig\">\n              <jats:sc>Skolem<\/jats:sc>\n            <\/jats:xref>\n            -hard to compute for polynomial probabilistic loops without branching statements. Finally, we identify a class of probabilistic loops for which the strongest polynomial moment invariant is computable and provide an algorithm for it.\n          <\/jats:p>","DOI":"10.1145\/3632872","type":"journal-article","created":{"date-parts":[[2024,1,5]],"date-time":"2024-01-05T20:48:51Z","timestamp":1704487731000},"page":"882-910","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":5,"title":["Strong Invariants Are Hard: On the Hardness of Strongest Polynomial Invariants for (Probabilistic) Programs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0006-2909-2297","authenticated-orcid":false,"given":"Julian","family":"M\u00fcllner","sequence":"first","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2006-3741","authenticated-orcid":false,"given":"Marcel","family":"Moosbrugger","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8299-2714","authenticated-orcid":false,"given":"Laura","family":"Kov\u00e1cs","sequence":"additional","affiliation":[{"name":"TU Wien, Vienna, Austria"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2024,1,5]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","unstructured":"Christel Baier Florian Funke Simon Jantsch Toghrul Karimov Engel Lefaucheux Florian Luca Jo\u00ebl Ouaknine David Purser Markus A. Whiteland and James Worrell. 2021. The Orbit Problem for Parametric Linear Dynamical Systems. In Proc. of CONCUR. https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2021.28 10.4230\/LIPIcs.CONCUR.2021.28","DOI":"10.4230\/LIPIcs.CONCUR.2021.28"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Thomas Espitau Luis Mar\u00eda Ferrer Fioriti and Justin Hsu. 2016. Synthesizing Probabilistic Invariants via Doob\u2019s Decomposition. In Proc. of CAV. https:\/\/doi.org\/10.1007\/978-3-319-41528-4_310.1007\/978-3-319-41528-4_3","DOI":"10.1007\/978-3-319-41528-4_3"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Benjamin Gr\u00e9goire and Santiago Zanella B\u00e9guelin. 2012a. Probabilistic Relational Hoare Logics for Computer-Aided Security Proofs. In Proc. of MPC. https:\/\/doi.org\/10.1007\/978-3-642-31113-010.1007\/978-3-642-31113-0","DOI":"10.1007\/978-3-642-31113-0"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1017\/9781108770750"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","unstructured":"Gilles Barthe Boris K\u00f6pf Federico Olmedo and Santiago Zanella B\u00e9guelin. 2012b. Probabilistic Relational Reasoning for Differential Privacy. In Proc. of POPL. https:\/\/doi.org\/10.1145\/2103656.210367010.1145\/2103656.2103670","DOI":"10.1145\/2103656.2103670"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","unstructured":"Ezio Bartocci Laura Kov\u00e1cs and Miroslav Stankovic. 2019. Automatic Generation of Moment-Based Invariants for Prob-Solvable Loops. In Proc. of ATVA. https:\/\/doi.org\/10.1007\/978-3-030-31784-3_1510.1007\/978-3-030-31784-3_15","DOI":"10.1007\/978-3-030-31784-3_15"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","unstructured":"Kevin Batz Mingshuai Chen Sebastian Junges Benjamin Lucien Kaminski Joost-Pieter Katoen and Christoph Matheja. 2023a. Probabilistic Program Verification via Inductive Synthesis of Inductive Invariants. In Proc. of TACAS. https:\/\/doi.org\/10.1007\/978-3-031-30820-8_2510.1007\/978-3-031-30820-8_25","DOI":"10.1007\/978-3-031-30820-8_25"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","unstructured":"Kevin Batz Mingshuai Chen Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Philipp Schr\u00f6er. 2021. Latticed k-Induction with an Application to Probabilistic Programs. In Proc. of CAV. https:\/\/doi.org\/10.1007\/978-3-030-81688-9_2510.1007\/978-3-030-81688-9_25","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","unstructured":"Kevin Batz Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Lena Verscht. 2023b. A Calculus for Amortized Expected Runtimes. Proc. ACM Program. Lang. POPL (2023). https:\/\/doi.org\/10.1145\/357126010.1145\/3571260","DOI":"10.1145\/3571260"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","unstructured":"Yuri Bilu Florian Luca Joris Nieuwveld Jo\u00ebl Ouaknine David Purser and James Worrell. 2022. Skolem Meets Schanuel. In Proc. of MFCS. https:\/\/doi.org\/10.4230\/LIPIcs.MFCS.2022.2010.4230\/LIPIcs.MFCS.2022.20","DOI":"10.4230\/LIPIcs.MFCS.2022.20"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","unstructured":"Bruno Buchberger. 2006. Bruno Buchberger\u2019s PhD thesis 1965: An algorithm for finding the basis elements of the residue class ring of a zero dimensional polynomial ideal. J. Symb. Comput. (2006). https:\/\/doi.org\/10.1016\/j.jsc.2005.09.00710.1016\/j.jsc.2005.09.007","DOI":"10.1016\/j.jsc.2005.09.007"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","unstructured":"Micha\u00ebl Cadilhac Filip Mazowiecki Charles Paperman Michal Pilipczuk and G\u00e9raud S\u00e9nizergues. 2020. On Polynomial Recursive Sequences. In Proc. of ICALP. https:\/\/doi.org\/10.4230\/LIPIcs.ICALP.2020.11710.4230\/LIPIcs.ICALP.2020.117","DOI":"10.4230\/LIPIcs.ICALP.2020.117"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","unstructured":"Aleksandar Chakarov and Sriram Sankaranarayanan. 2014. Expectation Invariants for Probabilistic Program Loops as Fixed Points. In Proc. of SAS. https:\/\/doi.org\/10.1007\/978-3-319-10936-7_610.1007\/978-3-319-10936-7_6","DOI":"10.1007\/978-3-319-10936-7_6"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","unstructured":"Krishnendu Chatterjee Petr Novotn\u00fd and Dorde Zikelic. 2017. Stochastic invariants for probabilistic termination. In Proc. of POPL. https:\/\/doi.org\/10.1145\/3009837.300987310.1145\/3009837.3009873","DOI":"10.1145\/3009837.3009873"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","unstructured":"Ventsislav Chonev Jo\u00ebl Ouaknine and James Worrell. 2013. The orbit problem in higher dimensions. In Proc. of STOC. https:\/\/doi.org\/10.1145\/2488608.248872810.1145\/2488608.2488728","DOI":"10.1145\/2488608.2488728"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","unstructured":"Ventsislav Chonev Jo\u00ebl Ouaknine and James Worrell. 2015. The Polyhedron-Hitting Problem. In Proc. of SODA. https:\/\/doi.org\/10.1137\/1.9781611973730.6410.1137\/1.9781611973730.64","DOI":"10.1137\/1.9781611973730.64"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","unstructured":"David A. Cox John Little and Donal O\u2019Shea. 1997. Ideals varieties and algorithms - an introduction to computational algebraic geometry and commutative algebra. https:\/\/doi.org\/10.1137\/103517110.1137\/1035171","DOI":"10.1137\/1035171"},{"key":"e_1_3_1_19_1","unstructured":"Thao Dang and Romain Testylier. 2012. Reachability Analysis for Polynomial Dynamical Systems Using the Bernstein Expansion. Reliab. Comput. (2012)."},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","unstructured":"Tommaso Dreossi Thao Dang and Carla Piazza. 2017. Reachability computation for polynomial dynamical systems. Formal Methods Syst. Des. (2017). https:\/\/doi.org\/10.1007\/s10703-016-0266-310.1007\/s10703-016-0266-3","DOI":"10.1007\/s10703-016-0266-3"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","unstructured":"Catherine Dufourd Alain Finkel and Philippe Schnoebelen. 1998. Reset Nets Between Decidability and Undecidability. In Proc. of ICALP. https:\/\/doi.org\/10.1007\/BFb005504410.1007\/BFb0055044","DOI":"10.1007\/BFb0055044"},{"key":"e_1_3_1_22_1","doi-asserted-by":"crossref","unstructured":"Graham Everest Alfred J. van der Poorten Igor E. Shparlinski and Thomas Ward. 2003. Recurrence Sequences. American Mathematical Society. ISBN 978-0-8218-3387-2.","DOI":"10.1090\/surv\/104"},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","unstructured":"Azadeh Farzan and Zachary Kincaid. 2015. Compositional Recurrence Analysis. In FMCAD. https:\/\/doi.org\/10.1109\/FMCAD.2015.754225310.1109\/FMCAD.2015.7542253","DOI":"10.1109\/FMCAD.2015.7542253"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","unstructured":"Alain Finkel Stefan G\u00f6ller and Christoph Haase. 2013. Reachability in Register Machines with Polynomial Updates. In Proc. of MFCS. https:\/\/doi.org\/10.1007\/978-3-642-40313-2_3710.1007\/978-3-642-40313-2_37","DOI":"10.1007\/978-3-642-40313-2_37"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","unstructured":"Zoubin Ghahramani. 2015. Probabilistic Machine Learning and Artificial Intelligence. Nature (2015). https:\/\/doi.org\/10.1038\/nature1454110.1038\/nature14541","DOI":"10.1038\/nature14541"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","unstructured":"Friedrich Gretz Joost-Pieter Katoen and Annabelle McIver. 2013. Prinsys - On a Quest for Probabilistic Loop Invariants. In Proc. of QEST. https:\/\/doi.org\/10.1007\/978-3-642-40196-1_1710.1007\/978-3-642-40196-1_17","DOI":"10.1007\/978-3-642-40196-1_17"},{"key":"e_1_3_1_27_1","unstructured":"John E. Hopcroft and Jeffrey D. Ullman. 1969. Formal languages and their relation to automata."},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","unstructured":"Ehud Hrushovski Jo\u00ebl Ouaknine Amaury Pouly and James Worrell. 2018. Polynomial Invariants for Affine Programs. In Proc. of LICS. https:\/\/doi.org\/10.1145\/3209108.320914210.1145\/3209108.3209142","DOI":"10.1145\/3209108.3209142"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","unstructured":"Ehud Hrushovski Jo\u00ebl Ouaknine Amaury Pouly and James Worrell. 2023. On Strongest Algebraic Program Invariants. J. ACM (2023). https:\/\/doi.org\/10.1145\/361431910.1145\/3614319","DOI":"10.1145\/3614319"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","unstructured":"Benjamin Lucien Kaminski Joost-Pieter Katoen and Christoph Matheja. 2019. On the hardness of analyzing probabilistic programs. Acta Inform. (2019). https:\/\/doi.org\/10.1007\/s00236-018-0321-110.1007\/s00236-018-0321-1","DOI":"10.1007\/s00236-018-0321-1"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","unstructured":"Benjamin Lucien Kaminski Joost-Pieter Katoen Christoph Matheja and Federico Olmedo. 2018. Weakest Precondition Reasoning for Expected Runtimes of Randomized Algorithms. J. ACM (2018). https:\/\/doi.org\/10.1145\/320810210.1145\/3208102","DOI":"10.1145\/3208102"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","unstructured":"Ravindran Kannan and Richard J. Lipton. 1980. The Orbit Problem is Decidable. In Proc. of STOC. https:\/\/doi.org\/10.1145\/800141.80467310.1145\/800141.804673","DOI":"10.1145\/800141.804673"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","unstructured":"Toghrul Karimov Engel Lefaucheux Jo\u00ebl Ouaknine David Purser Anton Varonka Markus A. Whiteland and James Worrell. 2022. What\u2019s decidable about linear loops? Proc. ACM Program. Lang. POPL (2022). https:\/\/doi.org\/10.1145\/349872710.1145\/3498727","DOI":"10.1145\/3498727"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","unstructured":"Michael Karr. 1976. Affine Relationships Among Variables of a Program. Acta Inform. (1976). https:\/\/doi.org\/10.1007\/BF0026849710.1007\/BF00268497","DOI":"10.1007\/BF00268497"},{"key":"e_1_3_1_35_1","volume-title":"Algorithms for Nonlinear Higher Order Difference Equations","author":"Kauers Manuel","year":"2005","unstructured":"Manuel Kauers. 2005. Algorithms for Nonlinear Higher Order Difference Equations. Ph.D. Dissertation. RISC, Johannes Kepler University, Linz."},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-7091-0445-3"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","unstructured":"Manuel Kauers and Burkhard Zimmermann. 2008. Computing the algebraic relations of C-finite sequences and multisequences. J. Symb. Comput. (2008). https:\/\/doi.org\/10.1016\/JJSC.2008.03.00210.1016\/JJSC.2008.03.002","DOI":"10.1016\/JJSC.2008.03.002"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","unstructured":"Zachary Kincaid Jason Breck John Cyphert and Thomas W. Reps. 2019. Closed forms for numerical loops. Proc. ACM Program. Lang. POPL (2019). https:\/\/doi.org\/10.1145\/329036810.1145\/3290368","DOI":"10.1145\/3290368"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","unstructured":"Zachary Kincaid John Cyphert Jason Breck and Thomas W. Reps. 2018. Non-linear reasoning for invariant synthesis. Proc. ACM Program. Lang. POPL (2018). https:\/\/doi.org\/10.1145\/315814210.1145\/3158142","DOI":"10.1145\/3158142"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","unstructured":"Zachary Kincaid Nicolas Koh and Shaowei Zhu. 2023. When Less Is More: Consequence-Finding in a Weak Theory of Arithmetic. Proc. ACM Program. Lang. POPL (2023). https:\/\/doi.org\/10.1145\/357123710.1145\/3571237","DOI":"10.1145\/3571237"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","unstructured":"Sang-Ki Ko Reino Niskanen and Igor Potapov. 2018. Reachability Problems in Nondeterministic Polynomial Maps on the Integers. In Proc. of DLT. https:\/\/doi.org\/10.1007\/978-3-319-98654-8_3810.1007\/978-3-319-98654-8_38","DOI":"10.1007\/978-3-319-98654-8_38"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","unstructured":"Andrey Kofnov Marcel Moosbrugger Miroslav Stankovic Ezio Bartocci and Efstathia Bura. 2022. Moment-Based Invariants for Probabilistic Loops with Non-polynomial Assignments. In Proc. of QEST. https:\/\/doi.org\/10.1007\/978-3-031-16336-4_1 10.1007\/978-3-031-16336-4_1","DOI":"10.1007\/978-3-031-16336-4_1"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","unstructured":"Laura Kov\u00e1cs. 2008. Reasoning Algebraically About P-Solvable Loops. In Proc. of TACAS. https:\/\/doi.org\/10.1007\/978-3-540-78800-3_18 10.1007\/978-3-540-78800-3_18","DOI":"10.1007\/978-3-540-78800-3_18"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","unstructured":"Laura Kov\u00e1cs and Anton Varonka. 2023. What Else is Undecidable About Loops?. In Proc. of RAMiCS. https:\/\/doi.org\/10.1007\/978-3-031-28083-2_11 10.1007\/978-3-031-28083-2_11","DOI":"10.1007\/978-3-031-28083-2_11"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 1983. A Probabilistic PDL. In Proc. of STOC. https:\/\/doi.org\/10.1145\/800061.808758 10.1145\/800061.808758","DOI":"10.1145\/800061.808758"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","unstructured":"Dexter Kozen. 1985. A Probabilistic PDL. J. Comput. Syst. Sci. (1985). https:\/\/doi.org\/10.1016\/0022-0000(85)90012-1 10.1016\/0022-0000(85)90012-1","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","unstructured":"Richard Lipton Florian Luca Joris Nieuwveld Jo\u00ebl Ouaknine David Purser and James Worrell. 2022. On the Skolem Problem and the Skolem Conjecture. In Proc. of LICS. https:\/\/doi.org\/10.1145\/3531130.3533328 10.1145\/3531130.3533328","DOI":"10.1145\/3531130.3533328"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","unstructured":"Annabelle McIver and Carroll Morgan. 2005. Abstraction Refinement and Proof for Probabilistic Systems. https:\/\/doi.org\/10.1007\/b138392 10.1007\/b138392","DOI":"10.1007\/b138392"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","unstructured":"Marcel Moosbrugger Miroslav Stankovic Ezio Bartocci and Laura Kov\u00e1cs. 2022. This is the moment for probabilistic loops. Proc. ACM Program. Lang. OOPSLA2 (2022). https:\/\/doi.org\/10.1145\/3563341 10.1145\/3563341","DOI":"10.1145\/3563341"},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","unstructured":"Markus M\u00fcller-Olm and Helmut Seidl. 2004a. Computing polynomial program invariants. Inf. Process. Lett. (2004). https:\/\/doi.org\/10.1016\/j.ipl.2004.05.004 10.1016\/j.ipl.2004.05.004","DOI":"10.1016\/j.ipl.2004.05.004"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","unstructured":"Markus M\u00fcller-Olm and Helmut Seidl. 2004b. A Note on Karr\u2019s Algorithm. In Proc. of ICALP. https:\/\/doi.org\/10.1007\/978-3-540-27836-8_85 10.1007\/978-3-540-27836-8_85","DOI":"10.1007\/978-3-540-27836-8_85"},{"key":"e_1_3_1_52_1","volume-title":"Exact Inference for Probabilistic Loops","author":"M\u00fcllner Julian","year":"2023","unstructured":"Julian M\u00fcllner. 2023. Exact Inference for Probabilistic Loops. Master\u2019s thesis. Technische Universit\u00e4t Wien."},{"key":"e_1_3_1_53_1","doi-asserted-by":"crossref","unstructured":"Emil L. Post. 1946. A variant of a recursively unsolvable problem. Bull. Am. Math. Soc. (1946).","DOI":"10.1090\/S0002-9904-1946-08555-9"},{"key":"e_1_3_1_54_1","unstructured":"Terrence Tao. 2008. Structure and Randomness. American Mathematical Society. ISBN 0-8218-4695-7."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632872","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3632872","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,7,4]],"date-time":"2025-07-04T20:07:39Z","timestamp":1751659659000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3632872"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,1,2]]},"references-count":53,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2024,1,2]]}},"alternative-id":["10.1145\/3632872"],"URL":"https:\/\/doi.org\/10.1145\/3632872","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,1,2]]},"assertion":[{"value":"2024-01-05","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}