{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:04:06Z","timestamp":1767927846152,"version":"3.49.0"},"reference-count":43,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2019,7,26]],"date-time":"2019-07-26T00:00:00Z","timestamp":1564099200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1718220"],"award-info":[{"award-number":["1718220"]}],"id":[{"id":"10.13039\/100000001","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":[[2019,7,26]]},"abstract":"<jats:p>Relational cost analysis aims at formally establishing bounds on the difference in the evaluation costs of two programs. As a particular case, one can also use relational cost analysis to establish bounds on the difference in the evaluation cost of the same program on two different inputs. One way to perform relational cost analysis is to use a relational type-and-effect system that supports reasoning about relations between two executions of two programs.<\/jats:p>\n          <jats:p>Building on this basic idea, we present a type-and-effect system, called ARel, for reasoning about the relative cost of array-manipulating, higher-order functional-imperative programs. The key ingredient of our approach is a new lightweight type refinement discipline that we use to track relations (differences) between two mutable arrays. This discipline combined with Hoare-style triples built into the types allows us to express and establish precise relative costs of several interesting programs which imperatively update their data. We have implemented ARel using ideas from bidirectional type checking.<\/jats:p>","DOI":"10.1145\/3341696","type":"journal-article","created":{"date-parts":[[2019,7,29]],"date-time":"2019-07-29T20:55:51Z","timestamp":1564433751000},"page":"1-29","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":8,"title":["Relational cost analysis for functional-imperative programs"],"prefix":"10.1145","volume":"3","author":[{"given":"Weihao","family":"Qu","sequence":"first","affiliation":[{"name":"SUNY Buffalo, USA"}],"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"}]}],"member":"320","published-online":{"date-parts":[[2019,7,26]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/11693024_6"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1480881.1480925"},{"key":"e_1_2_2_3_1","unstructured":"Amal G Ahmed. 2004. Semantics of types for mutable state.   Amal G Ahmed. 2004. Semantics of types for mutable state."},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/504709.504712"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_6"},{"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\/2535838.2535847"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2676726.2677000"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/964001.964003"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2535838.2535869"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2967973.2968602"},{"key":"e_1_2_2_12_1","volume-title":"The Alt-Ergo automated theorem prover","author":"Bobot Fran\u00e7ois","year":"2008"},{"key":"e_1_2_2_13_1","volume-title":"Conf. (TACAS).","author":"Brockschmidt Marc","year":"2014"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737955"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009858"},{"key":"e_1_2_2_16_1","volume-title":"Interactive Theorem Proving - 6th International Conference, ITP.","author":"Chargu\u00e9raud Arthur"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951950"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3314221.3314603"},{"key":"e_1_2_2_19_1","volume-title":"Tukey","author":"Cooley James W.","year":"1965"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2011.22"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328457"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_8"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429113"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/507635.507666"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2005.02.006"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926427"},{"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\/1882362.1882405"},{"key":"e_1_2_2_29_1","volume-title":"Arrays and References in Resource Aware ML. In The 2nd International Conference on Formal Structures for Computation and Deduction, FSCD.","author":"Lichtman Benjamin","year":"2017"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491522.2491523"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796808006953"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796811000165"},{"key":"e_1_2_2_33_1","volume-title":"Verifying and Synthesizing ConstantResource Implementations with Types. In 2017 IEEE Symposium on Security &amp; Privacy.","author":"Ngo Van Chan","year":"2017"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/646005.673740"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/345099.345100"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158124"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/182409.182439"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-08867-9_50"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429111"},{"key":"e_1_2_2_40_1","volume-title":"Computer Aided Verification - 29th International Conference, CAV.","author":"Unno Hiroshi"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3133903"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292560"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694372"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341696","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341696","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3341696","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T22:41:30Z","timestamp":1750200090000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3341696"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2019,7,26]]},"references-count":43,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2019,7,26]]}},"alternative-id":["10.1145\/3341696"],"URL":"https:\/\/doi.org\/10.1145\/3341696","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2019,7,26]]},"assertion":[{"value":"2019-07-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}