{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,10]],"date-time":"2026-04-10T03:13:01Z","timestamp":1775790781142,"version":"3.50.1"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2017,12,27]],"date-time":"2017-12-27T00:00:00Z","timestamp":1514332800000},"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":[[2018,1]]},"abstract":"<jats:p>\n            Formal frameworks for cost analysis of programs have been widely studied in the unary setting and, to a limited extent, in the relational setting. However, many of these frameworks focus only on the cost aspect, largely side-lining functional properties that are often a prerequisite for cost analysis, thus leaving many interesting programs out of their purview. In this paper, we show that elegant, simple, expressive proof systems combining cost analysis and functional properties can be built by combining already known ingredients: higher-order refinements and cost monads. Specifically, we derive two syntax-directed proof systems, U\n            <jats:sup>C<\/jats:sup>\n            and R\n            <jats:sup>C<\/jats:sup>\n            , for unary and relational cost analysis, by adding a cost monad to a (syntax-directed) logic of higher-order programs. We study the metatheory of the systems, show that several nontrivial examples can be verified in them, and prove that existing frameworks for cost analysis (RelCost and RAML) can be embedded in them.\n          <\/jats:p>","DOI":"10.1145\/3158124","type":"journal-article","created":{"date-parts":[[2017,12,29]],"date-time":"2017-12-29T14:21:49Z","timestamp":1514557309000},"page":"1-32","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":30,"title":["Monadic refinements for relational cost analysis"],"prefix":"10.1145","volume":"2","author":[{"given":"Ivan","family":"Radi\u010dek","sequence":"first","affiliation":[{"name":"Vienna University of Technology, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Gilles","family":"Barthe","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marco","family":"Gaboardi","sequence":"additional","affiliation":[{"name":"SUNY Buffalo, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Deepak","family":"Garg","sequence":"additional","affiliation":[{"name":"MPI-SWS, Germany"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Florian","family":"Zuleger","sequence":"additional","affiliation":[{"name":"Vienna University of Technology, Austria"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2017,12,27]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"crossref","unstructured":"Alejandro Aguirre Gilles Barthe Lars Birkedal Ale\u0161 Bizjak Marco Gaboardi and Deepak Garg. 2017a. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. (2017). In preparation.  Alejandro Aguirre Gilles Barthe Lars Birkedal Ale\u0161 Bizjak Marco Gaboardi and Deepak Garg. 2017a. Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus. (2017). In preparation.","DOI":"10.1007\/978-3-319-89884-1_8"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110265"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.07.009"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15769-1_8"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(2:17)2011"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110287"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784753"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535847"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2011.02.007"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2866575"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_2_2_14_1","volume-title":"Hans Bugge Grathwohl, and Lars Birkedal","author":"Clouston Ranald","year":"2016","unstructured":"Ranald Clouston , Ale\u0161 Bizjak , Hans Bugge Grathwohl, and Lars Birkedal . 2016 . The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science 12, 3 (2016). Ranald Clouston, Ale\u0161 Bizjak, Hans Bugge Grathwohl, and Lars Birkedal. 2016. The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types. Logical Methods in Computer Science 12, 3 (2016)."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/325694.325716"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429090"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2784731.2784749"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/93542.93564"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-12736-1_15"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507666"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480898"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1806596.1806630"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.006"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31424-7_64"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009842"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/604131.604148"},{"key":"e_1_2_2_30_1","volume-title":"Categorical Logic and Type Theory","author":"Jacobs Bart","unstructured":"Bart Jacobs . 1999. Categorical Logic and Type Theory . Elsevier . Studies in Logic and the Foundations of Mathematics 141. Bart Jacobs. 1999. Categorical Logic and Type Theory. Elsevier. Studies in Logic and the Foundations of Mathematics 141."},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706327"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9398-9"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009874"},{"key":"e_1_2_2_34_1","volume-title":"Notions of computations and monads. 93, 1","author":"Moggi Eugenio","year":"1991","unstructured":"Eugenio Moggi . 1991. Notions of computations and monads. 93, 1 ( 1991 ), 55\u201392. Eugenio Moggi. 1991. Notions of computations and monads. 93, 1 (1991), 55\u201392."},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491522.2491523"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2017.53"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_2_2_39_1","volume-title":"29th Int\u2019l. Conference on Logic Programming (ICLP\u201913)","volume":"13","author":"Serrano A.","unstructured":"A. Serrano , P. Lopez-Garcia , F. Bueno , and M. V. Hermenegildo . 2013. Sized Type Analysis for Logic Programs. In Theory and Practice of Logic Programming , 29th Int\u2019l. Conference on Logic Programming (ICLP\u201913) Special Issue, On-line Supplement , Vol. 13 . Cambridge U. Press, 1\u201314. A. Serrano, P. Lopez-Garcia, F. Bueno, and M. V. Hermenegildo. 2013. Sized Type Analysis for Logic Programs. In Theory and Practice of Logic Programming, 29th Int\u2019l. Conference on Logic Programming (ICLP\u201913) Special Issue, On-line Supplement, Vol. 13. Cambridge U. Press, 1\u201314."},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10817-016-9402-4"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837655"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/601775.601776"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133903"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-23702-7_22"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158124","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3158124","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:30Z","timestamp":1750212690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3158124"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,27]]},"references-count":45,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2018,1]]}},"alternative-id":["10.1145\/3158124"],"URL":"https:\/\/doi.org\/10.1145\/3158124","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2017,12,27]]},"assertion":[{"value":"2017-12-27","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}