{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T08:21:25Z","timestamp":1770279685295,"version":"3.49.0"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","license":[{"start":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T00:00:00Z","timestamp":1728345600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["CCF-2006535, CNS-2244494, CCF-2327738"],"award-info":[{"award-number":["CCF-2006535, CNS-2244494, CCF-2327738"]}],"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":[[2024,10,8]]},"abstract":"<jats:p>\n                    Effect and coeffect tracking integrate many types of compile-time analysis, such as cost, liveness, or dataflow, directly into a language\u2019s type system. In this paper, we investigate the addition of effect and coeffect tracking to the type system of call-by-push-value (CBPV), a computational model useful in compilation for its isolation of effects and for its ability to cleanly express both call-by-name and call-by-value computations. Our main result is\n                    <jats:italic toggle=\"yes\">effect-and-coeffect soundness<\/jats:italic>\n                    , which asserts that the type system accurately bounds the effects that the program may trigger during execution and accurately tracks the demands that the program may make on its environment. This result holds for two different dynamic semantics: a generic one that can be adapted for different coeffects and one that is adapted for reasoning about resource usage. In particular, the second semantics discards the evaluation of unused values and pure computations while ensuring that effectful computations are always evaluated, even if their results are not required. Our results have been mechanized using the Coq proof assistant.\n                  <\/jats:p>","DOI":"10.1145\/3689750","type":"journal-article","created":{"date-parts":[[2024,10,8]],"date-time":"2024-10-08T03:23:04Z","timestamp":1728357784000},"page":"1108-1134","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Effects and Coeffects in Call-by-Push-Value"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-6717-9586","authenticated-orcid":false,"given":"Cassia","family":"Torczon","sequence":"first","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0002-5515-6099","authenticated-orcid":false,"given":"Emmanuel","family":"Su\u00e1rez Acevedo","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0006-1844-3856","authenticated-orcid":false,"given":"Shubh","family":"Agrawal","sequence":"additional","affiliation":[{"name":"University of Michigan, Ann Arbor, USA"}]},{"ORCID":"https:\/\/orcid.org\/0009-0004-6451-5107","authenticated-orcid":false,"given":"Joey","family":"Velez-Ginorio","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-6756-9168","authenticated-orcid":false,"given":"Stephanie","family":"Weirich","sequence":"additional","affiliation":[{"name":"University of Pennsylvania, Philadelphia, USA"}]}],"member":"320","published-online":{"date-parts":[[2024,10,8]]},"reference":[{"key":"e_1_3_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408972"},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/3607862"},{"key":"e_1_3_1_4_1","unstructured":"Amal Ahmed Matthew Fluet and Greg Morrisett. 2007. L3 : A Linear Language with Locations. Fundam. Informaticae 77 4 (2007) 397\u2013449. http:\/\/content.iospress.com\/articles\/fundamenta-informaticae\/fi77-4-06"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209189"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158093"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/3622843"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3527320"},{"key":"e_1_3_1_9_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2021.9"},{"key":"e_1_3_1_10_1","doi-asserted-by":"crossref","first-page":"351","DOI":"10.1007\/978-3-642-54833-8_19","volume-title":"Programming Languages and Systems","author":"Brunel Alo\u00efs","year":"2014","unstructured":"Alo\u00efs Brunel, Marco Gaboardi, Damiano Mazza, and Steve Zdancewic. 2014. A Core Quantitative Coeffect Calculus. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 351\u2013370."},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434331"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000039"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/3498692"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/3450952"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04027-6"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/exs025"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3110257"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/3293880.3294097"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_3_1_20_1","unstructured":"Dmitri Garbuzov William Mansky Christine Rizkallah and Steve Zdancewic. 2018. Structural Operational Semantics for Control Flow Graph Machines. arXiv:1805.05400 [cs.PL] https:\/\/arxiv.org\/abs\/1805.05400"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/3209108.3209149"},{"key":"e_1_3_1_22_1","doi-asserted-by":"crossref","first-page":"331","DOI":"10.1007\/978-3-642-54833-8_18","volume-title":"Programming Languages and Systems","author":"Ghica Dan R.","year":"2014","unstructured":"Dan R. Ghica and Alex I. Smith. 2014. Bounded Linear Types in a Resource Semiring. In Programming Languages and Systems, Zhong Shao (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg, 331\u2013350."},{"key":"e_1_3_1_23_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2024.15"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500590"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103698"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535846"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-99336-8_16"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.4204\/eptcs.153.8"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(04)80568-1"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0954-6"},{"key":"e_1_3_1_31_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-006-0480-6"},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3537668.3537670"},{"key":"e_1_3_1_33_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1515\/comp-2018-0009"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-17184-1_9"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/888251.888271"},{"key":"e_1_3_1_39_1","unstructured":"Max S. New. 2019. From Call-by-push-value to Stack-based TAL? Presentation at LOLA 2019. https:\/\/maxsnew.com\/docs\/cbpv-stal-lola-2019.pdf"},{"key":"e_1_3_1_40_1","unstructured":"Dominic Orchard and Harley Eades III. 2022. The Granule Project. https:\/\/granule-project.github.io\/"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2633357.2633368"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371126"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341712"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2008.45"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434308"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1863543.1863568"},{"key":"e_1_3_1_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408977"},{"key":"e_1_3_1_50_1","doi-asserted-by":"crossref","first-page":"523","DOI":"10.1007\/978-3-319-94821-8_31","volume-title":"Interactive Theorem Proving","author":"Rizkallah Christine","year":"2018","unstructured":"Christine Rizkallah, Dmitri Garbuzov, and Steve Zdancewic. 2018. A Formal Equational Theory for Call-By-Push-Value. In Interactive Theorem Proving, Jeremy Avigad and Assia Mahboubi (Eds.). Springer International Publishing, Cham, 523\u2013541."},{"key":"e_1_3_1_51_1","unstructured":"Ulrich Sch\u00f6pp. 2015. Computation-by-Interaction for Structuring Low-Level Computation. Ph. D. Dissertation. Habilitation thesis Ludwig-Maximilians-Universit\u00e4t M\u00fcnchen."},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10958-008-9013-7"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1046"},{"key":"e_1_3_1_54_1","doi-asserted-by":"crossref","unstructured":"Cassia Torczon Emmanuel Su\u00e1rez Acevedo Shubh Agrawal Joey Velez-Ginorio and Stephanie Weirich. 2024a. Effects and Coeffects in Call-By-Push-Value (Extended Version). arXiv:2311.11795 [cs.PL]","DOI":"10.1145\/3689750"},{"key":"e_1_3_1_55_1","doi-asserted-by":"publisher","unstructured":"Cassia Torczon Emmanuel Suarez Acevedo Shubh Agrawal Joey Velez-Ginorio and Stephanie Weirich. 2024b. Artifact associated with \u201cEffects and Co-effects in Call-By-Push-Value\u201d. https:\/\/doi.org\/10.5281\/zenodo.12654518 10.5281\/zenodo.12654518","DOI":"10.5281\/zenodo.12654518"},{"key":"e_1_3_1_56_1","unstructured":"Verse development team. 2023. Verse Language Reference. Epic Games. https:\/\/dev.epicgames.com\/documentation\/en-us\/uefn\/verse-language-reference."},{"key":"e_1_3_1_57_1","doi-asserted-by":"publisher","DOI":"10.1145\/601775.601776"},{"key":"e_1_3_1_58_1","unstructured":"Maxi Wuttke. 2021. Sound and Relatively Complete Coeffect and effect refinement type systems for call-by-push-value PCF. Master\u2019s thesis. Universit\u00e4t des Sarrlandes."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689750","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3689750","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T09:11:04Z","timestamp":1770196264000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3689750"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,10,8]]},"references-count":57,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2024,10,8]]}},"alternative-id":["10.1145\/3689750"],"URL":"https:\/\/doi.org\/10.1145\/3689750","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,10,8]]},"assertion":[{"value":"2024-04-06","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-10-08","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}