{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,23]],"date-time":"2026-07-23T20:12:28Z","timestamp":1784837548381,"version":"3.55.0"},"reference-count":63,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"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":["787914"],"award-info":[{"award-number":["787914"]}],"id":[{"id":"10.13039\/501100000781","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001659","name":"German Research Foundation","doi-asserted-by":"crossref","award":["2236"],"award-info":[{"award-number":["2236"]}],"id":[{"id":"10.13039\/501100001659","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":[[2022,4,29]]},"abstract":"<jats:p>We study weighted programming, a programming paradigm for specifying mathematical models. More specifically, the weighted programs we investigate are like usual imperative programs with two additional features: (1) nondeterministic branching and (2) weighting execution traces. Weights can be numbers but also other objects like words from an alphabet, polynomials, formal power series, or cardinal numbers. We argue that weighted programming as a paradigm can be used to specify mathematical models beyond probability distributions (as is done in probabilistic programming). We develop weakest-precondition- and weakest-liberal-precondition-style calculi \u00e0 la Dijkstra for reasoning about mathematical models specified by weighted programs. We present several case studies. For instance, we use weighted programming to model the ski rental problem \u2014 an optimization problem. We model not only the optimization problem itself, but also the best deterministic online algorithm for solving this problem as weighted programs. By means of weakest-precondition-style reasoning, we can determine the competitive ratio of the online algorithm on source code level.<\/jats:p>","DOI":"10.1145\/3527310","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-30","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":17,"title":["Weighted programming: a programming paradigm for specifying mathematical models"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-8705-2564","authenticated-orcid":false,"given":"Kevin","family":"Batz","sequence":"first","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2176-5075","authenticated-orcid":false,"given":"Adrian","family":"Gallus","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5185-2324","authenticated-orcid":false,"given":"Benjamin Lucien","family":"Kaminski","sequence":"additional","affiliation":[{"name":"Saarland University, Germany \/ University College London, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6143-1926","authenticated-orcid":false,"given":"Joost-Pieter","family":"Katoen","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-1084-6408","authenticated-orcid":false,"given":"Tobias","family":"Winkler","sequence":"additional","affiliation":[{"name":"RWTH Aachen University, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Handbook of Logic in Computer Science. 3","author":"Abramsky Samson","unstructured":"Samson Abramsky . 1994. Handbook of Logic in Computer Science. 3 , Clarendon Press . http:\/\/www.cs.bham.ac.uk\/~axj\/papers.html Samson Abramsky. 1994. Handbook of Logic in Computer Science. 3, Clarendon Press. http:\/\/www.cs.bham.ac.uk\/~axj\/papers.html"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2020.09.002"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.3233\/978-1-61499-495-4-1"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1137\/1.9781611973068.91"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1721837.1721844"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-1674-2"},{"key":"e_1_2_1_7_1","volume-title":"On the Resolution Semiring. (Sur le Semi-anneau de R\u00e9solution). Ph. D. Dissertation","author":"Bagnol Marc","unstructured":"Marc Bagnol . 2014. On the Resolution Semiring. (Sur le Semi-anneau de R\u00e9solution). Ph. D. Dissertation . Aix-Marseille University , Aix-en- Provence, France . Marc Bagnol. 2014. On the Resolution Semiring. (Sur le Semi-anneau de R\u00e9solution). Ph. D. Dissertation. Aix-Marseille University, Aix-en-Provence, France."},{"key":"e_1_2_1_8_1","volume-title":"Principles of Model Checking","author":"Baier Christel","unstructured":"Christel Baier and Joost-Pieter Katoen . 2008. Principles of Model Checking . MIT Press . Christel Baier and Joost-Pieter Katoen. 2008. Principles of Model Checking. MIT Press."},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.18653\/v1\/2020.iwpt-1.8"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-81688-9_25"},{"key":"e_1_2_1_11_1","volume-title":"Joost-Pieter Katoen, and Tobias Winkler.","author":"Batz Kevin","year":"2022","unstructured":"Kevin Batz , Adrian Gallus , Benjamin Lucien Kaminski , Joost-Pieter Katoen, and Tobias Winkler. 2022 . Weighted Programming. CoRR , abs\/2202.07577 (2022), https:\/\/doi.org\/10.48550\/arXiv.2202.07577 Kevin Batz, Adrian Gallus, Benjamin Lucien Kaminski, Joost-Pieter Katoen, and Tobias Winkler. 2022. Weighted Programming. CoRR, abs\/2202.07577 (2022), https:\/\/doi.org\/10.48550\/arXiv.2202.07577"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3290347"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ijar.2020.08.001"},{"key":"e_1_2_1_14_1","unstructured":"Stefano Bistarelli Ugo Montanari and Francesca Rossi. 1997. Semiring-based Constraint Logic Programming. In IJCAI (1). Morgan Kaufmann 352\u2013357.  Stefano Bistarelli Ugo Montanari and Francesca Rossi. 1997. Semiring-based Constraint Logic Programming. In IJCAI (1). Morgan Kaufmann 352\u2013357."},{"key":"e_1_2_1_15_1","volume-title":"Online Computation and Competitive Analysis","author":"Borodin Allan","unstructured":"Allan Borodin and Ran El-Yaniv . 1998. Online Computation and Competitive Analysis . Cambridge University Press . Allan Borodin and Ran El-Yaniv. 1998. Online Computation and Competitive Analysis. Cambridge University Press."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_19"},{"key":"e_1_2_1_17_1","volume-title":"Modular and certified resource-bound analyses. Ph. D. Dissertation","author":"Carbonneaux Quentin","unstructured":"Quentin Carbonneaux . 2018. Modular and certified resource-bound analyses. Ph. D. Dissertation . Yale University . Quentin Carbonneaux. 2018. Modular and certified resource-bound analyses. Ph. D. Dissertation. Yale University."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89982-2_18"},{"key":"e_1_2_1_20_1","volume-title":"Generalized Absorptive Polynomials and Provenance Semantics for Fixed-Point Logic. CoRR, abs\/1910.07910","author":"Dannert Katrin M.","year":"2019","unstructured":"Katrin M. Dannert , Erich Gr\u00e4del , Matthias Naaf , and Val Tannen . 2019. Generalized Absorptive Polynomials and Provenance Semantics for Fixed-Point Logic. CoRR, abs\/1910.07910 ( 2019 ), https:\/\/doi.org\/10.48550\/arXiv.1910.07910 Katrin M. Dannert, Erich Gr\u00e4del, Matthias Naaf, and Val Tannen. 2019. Generalized Absorptive Polynomials and Provenance Semantics for Fixed-Point Logic. CoRR, abs\/1910.07910 (2019), https:\/\/doi.org\/10.48550\/arXiv.1910.07910"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/360933.360975"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500613"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-01492-5"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0029561"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-72019-3_9"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.fss.2014.11.008"},{"key":"e_1_2_1_27_1","first-page":"01","article-title":"Many-valued logic and semirings","volume":"13","author":"Gerla Brunella","year":"2003","unstructured":"Brunella Gerla . 2003 . Many-valued logic and semirings . Neural Network World , 13 (2003), 01 . Brunella Gerla. 2003. Many-valued logic and semirings. Neural Network World, 13 (2003), 01.","journal-title":"Neural Network World"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-54833-8_18"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.7561\/sacs.2019.2.141"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2593882.2593900"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2933575.2935319"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-3228-5_6"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.1002\/net.3230150211"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/360204.375719"},{"key":"e_1_2_1_35_1","unstructured":"Claire Jones. 1990. Probabilistic Non-Determinism. Ph. D. Dissertation. University of Edinburgh UK.  Claire Jones. 1990. Probabilistic Non-Determinism. Ph. D. Dissertation. University of Edinburgh UK."},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.18154\/RWTH-2019-01829"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.016"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-42749-2"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90012-1"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.1999.782610"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/343369.343378"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2013.36"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1109\/cacsd.2004.1393890"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/357084.357090"},{"key":"e_1_2_1_45_1","volume-title":"abs\/1108.2874","author":"Marcolli Matilde","year":"2011","unstructured":"Matilde Marcolli and Ryan Thorngren . 2011. Thermodynamic Semirings . CoRR , abs\/1108.2874 ( 2011 ), https:\/\/doi.org\/10.48550\/arXiv.1108.2874 Matilde Marcolli and Ryan Thorngren. 2011. Thermodynamic Semirings. CoRR, abs\/1108.2874 (2011), https:\/\/doi.org\/10.48550\/arXiv.1108.2874"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.4171\/jncg\/159"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/b138392"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/229542.229547"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-74970-7_38"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1090\/conm\/377\/06988"},{"key":"e_1_2_1_51_1","unstructured":"Russel O\u2019Conner. 2012. A Very General Method of Computing Shortest Paths. Personal blog entry. http:\/\/r6.ca\/blog\/20110808T035622Z.html  Russel O\u2019Conner. 2012. A Very General Method of Computing Shortest Paths. Personal blog entry. http:\/\/r6.ca\/blog\/20110808T035622Z.html"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.05.001"},{"key":"e_1_2_1_54_1","unstructured":"Marc Pouly. 2010. Semirings for Breakfast. https:\/\/marcpouly.ch\/pdf\/internal_100712.pdf Visited on 2022-03-21.  Marc Pouly. 2010. Semirings for Breakfast. https:\/\/marcpouly.ch\/pdf\/internal_100712.pdf Visited on 2022-03-21."},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1109\/lics.2002.1029817"},{"key":"e_1_2_1_56_1","volume-title":"Theory of Linear and Integer Programming","author":"Schrijver Alexander","unstructured":"Alexander Schrijver . 1999. Theory of Linear and Integer Programming . Wiley . Alexander Schrijver. 1999. Theory of Linear and Integer Programming. Wiley."},{"key":"e_1_2_1_57_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-40922-x_8"},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","DOI":"10.1162\/coli_a_00198"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341707"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","DOI":"10.1137\/0606031"},{"key":"e_1_2_1_61_1","unstructured":"G\u00fcnther J. Wirsching Markus Huber and Christian K\u00f6lbl. 2010. The confidence-probability semiring. Fakult\u00e4t f\u00fcr Angewandte Informatik.  G\u00fcnther J. Wirsching Markus Huber and Christian K\u00f6lbl. 2010. The confidence-probability semiring. Fakult\u00e4t f\u00fcr Angewandte Informatik."},{"key":"e_1_2_1_62_1","volume-title":"Quantitative Strongest Post. CoRR, abs\/2202.06765","author":"Zhang Linpeng","year":"2022","unstructured":"Linpeng Zhang and Benjamin Lucien Kaminski . 2022. Quantitative Strongest Post. CoRR, abs\/2202.06765 ( 2022 ), https:\/\/doi.org\/10.48550\/arXiv.2202.06765 Linpeng Zhang and Benjamin Lucien Kaminski. 2022. Quantitative Strongest Post. CoRR, abs\/2202.06765 (2022), https:\/\/doi.org\/10.48550\/arXiv.2202.06765"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527331"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527310","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527310","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:52Z","timestamp":1750191532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527310"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":63,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527310"],"URL":"https:\/\/doi.org\/10.1145\/3527310","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}