{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:45:43Z","timestamp":1780994743933,"version":"3.54.1"},"reference-count":56,"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-nd\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100001659","name":"Deutsche Forschungsgemeinschaft","doi-asserted-by":"publisher","award":["DFG-448316946"],"award-info":[{"award-number":["DFG-448316946"]}],"id":[{"id":"10.13039\/501100001659","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":[[2022,4,29]]},"abstract":"<jats:p>Reasoning about the use of external resources is an important aspect of many practical applications. Effect systems enable tracking such information in types, but at the cost of complicating signatures of common functions. Capabilities coupled with escape analysis offer safety and natural signatures, but are often overly coarse grained and restrictive. We present System C, which builds on and generalizes ideas from type-based escape analysis and demonstrates that capabilities and effects can be reconciled harmoniously. By assuming that all functions are second class, we can admit natural signatures for many common programs. By introducing a notion of boxed values, we can lift the restrictions of second-class values at the cost of needing to track degree-of-impurity information in types. The system we present is expressive enough to support effect handlers in full capacity. We practically evaluate System C in an implementation and prove its soundness.<\/jats:p>","DOI":"10.1145\/3527320","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":22,"title":["Effects, capabilities, and boxes: from scope-based reasoning to type-based reasoning and back"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9128-0391","authenticated-orcid":false,"given":"Jonathan Immanuel","family":"Brachth\u00e4user","sequence":"first","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8011-0506","authenticated-orcid":false,"given":"Philipp","family":"Schuster","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7057-0912","authenticated-orcid":false,"given":"Edward","family":"Lee","sequence":"additional","affiliation":[{"name":"University of Waterloo, Canada"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5769-6684","authenticated-orcid":false,"given":"Aleksander","family":"Boruch-Gruszecki","sequence":"additional","affiliation":[{"name":"EPFL, Switzerland"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/3434305"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1328438.1328443"},{"key":"e_1_2_2_3_1","volume-title":"Handbook of Logic in Computer Science (vol. 2): Background: Computational Structures","author":"Barendregt Henk P.","unstructured":"Henk P. Barendregt . 1992. Lambda Calculi with Types . In Handbook of Logic in Computer Science (vol. 2): Background: Computational Structures . Oxford University Press , New York, NY, USA . 117\u2013309. Henk P. Barendregt. 1992. Lambda Calculi with Types. In Handbook of Logic in Computer Science (vol. 2): Background: Computational Structures. Oxford University Press, New York, NY, USA. 117\u2013309."},{"key":"e_1_2_2_4_1","volume-title":"Coq\u2019Art:The Calculus of Inductive Constructions","author":"Bertot Yves","unstructured":"Yves Bertot and Pierre Cast\u00e9ran . 2004. Interactive Theorem Proving and Program Development , Coq\u2019Art:The Calculus of Inductive Constructions . Springer-Verlag . Yves Bertot and Pierre Cast\u00e9ran. 2004. Interactive Theorem Proving and Program Development, Coq\u2019Art:The Calculus of Inductive Constructions. Springer-Verlag."},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371116"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3136000.3136007"},{"key":"e_1_2_2_7_1","volume-title":"From Scope-Based Reasoning to Type-Based Reasoning and Back","author":"Brachth\u00e4user Jonathan Immanuel","unstructured":"Jonathan Immanuel Brachth\u00e4user , Philipp Schuster , Edward Lee , and Boruch-Gruszecki Aleksander . 2022. Effects, Capabilities, and Boxes : From Scope-Based Reasoning to Type-Based Reasoning and Back . University of T\u00fcbingen , Germany. https:\/\/se.informatik.uni-tuebingen.de\/publications\/brachthaeuser22effects Jonathan Immanuel Brachth\u00e4user, Philipp Schuster, Edward Lee, and Boruch-Gruszecki Aleksander. 2022. Effects, Capabilities, and Boxes: From Scope-Based Reasoning to Type-Based Reasoning and Back. University of T\u00fcbingen, Germany. https:\/\/se.informatik.uni-tuebingen.de\/publications\/brachthaeuser22effects"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3276481"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428194"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796820000027"},{"key":"e_1_2_2_11_1","unstructured":"Jonathan Immanuel Brachth\u00e4user and Daan Leijen. 2019. Programming with Implicit Values Functions and Control. Microsoft Research.  Jonathan Immanuel Brachth\u00e4user and Daan Leijen. 2019. Programming with Implicit Values Functions and Control. Microsoft Research."},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408993"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/2884781.2884798"},{"key":"e_1_2_2_14_1","volume-title":"Revisited. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications. ACM","author":"Cook William R.","year":"2009","unstructured":"William R. Cook . 2009 . On Understanding Data Abstraction , Revisited. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications. ACM , New York, NY, USA. 557\u2013572. William R. Cook. 2009. On Understanding Data Abstraction, Revisited. In Proceedings of the Conference on Object-Oriented Programming, Systems, Languages and Applications. ACM, New York, NY, USA. 557\u2013572."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/292540.292564"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_2_2_17_1","volume-title":"Effectively Tackling the Awkward Squad. In ML Workshop.","author":"Dolan Stephen","year":"2017","unstructured":"Stephen Dolan , Spiros Eliopoulos , Daniel Hillerstr\u00f6m , Anil Madhavapeddy , KC Sivaramakrishnan , and Leo White . 2017 . Effectively Tackling the Awkward Squad. In ML Workshop. Stephen Dolan, Spiros Eliopoulos, Daniel Hillerstr\u00f6m, Anil Madhavapeddy, KC Sivaramakrishnan, and Leo White. 2017. Effectively Tackling the Awkward Squad. In ML Workshop."},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796807006259"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73576"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/2951913.2951939"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2020.10"},{"key":"e_1_2_2_22_1","volume-title":"Proceedings of the Conference on Functional Programming Languages and Computer Architecture. ACM","author":"Gunter Carl A.","unstructured":"Carl A. Gunter , Didier R\u00e9my , and Jon G. Riecke . 1995. A Generalization of Exceptions and Control in ML-like Languages . In Proceedings of the Conference on Functional Programming Languages and Computer Architecture. ACM , New York, NY, USA. 12\u201323. Carl A. Gunter, Didier R\u00e9my, and Jon G. Riecke. 1995. A Generalization of Exceptions and Control in ML-like Languages. In Proceedings of the Conference on Functional Programming Languages and Computer Architecture. ACM, New York, NY, USA. 12\u201323."},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003025"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/1159803.1159808"},{"key":"e_1_2_2_25_1","volume-title":"Proceedings of the Symposium on Trends in Functional Programming. 297\u2013312","author":"Leijen Daan","year":"2005","unstructured":"Daan Leijen . 2005 . Extensible records with scoped labels . In Proceedings of the Symposium on Trends in Functional Programming. 297\u2013312 . Daan Leijen. 2005. Extensible records with scoped labels. In Proceedings of the Symposium on Trends in Functional Programming. 297\u2013312."},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.8"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/3122975.3122977"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009872"},{"key":"e_1_2_2_29_1","volume-title":"Call-by-Push-Value: A Subsuming Paradigm","author":"Levy Paul Blain","unstructured":"Paul Blain Levy . 1999. Call-by-Push-Value: A Subsuming Paradigm . In Typed Lambda Calculi and Applications, Jean-Yves Girard (Ed.). Springer Berlin Heidelberg , Berlin, Heidelberg . 228\u2013243. isbn:978-3-540-48959-7 Paul Blain Levy. 1999. Call-by-Push-Value: A Subsuming Paradigm. In Typed Lambda Calculi and Applications, Jean-Yves Girard (Ed.). Springer Berlin Heidelberg, Berlin, Heidelberg. 228\u2013243. isbn:978-3-540-48959-7"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_2_31_1","volume-title":"Encapsulating effects. Dagstuhl Reports, 8, 4","author":"Lindley Sam","year":"2018","unstructured":"Sam Lindley . 2018. Encapsulating effects. Dagstuhl Reports, 8, 4 ( 2018 ). Sam Lindley. 2018. Encapsulating effects. Dagstuhl Reports, 8, 4 (2018)."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3009837.3009897"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/73560.73564"},{"key":"e_1_2_2_34_1","volume-title":"31st European Conference on Object-Oriented Programming (ECOOP","author":"Melicher Darya","year":"2017","unstructured":"Darya Melicher , Yangqingwei Shi , Alex Potanin , and Jonathan Aldrich . 2017 . A capability-based module system for authority control . In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Darya Melicher, Yangqingwei Shi, Alex Potanin, and Jonathan Aldrich. 2017. A capability-based module system for authority control. In 31st European Conference on Object-Oriented Programming (ECOOP 2017)."},{"key":"e_1_2_2_35_1","volume-title":"Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation","author":"Miller Mark Samuel","year":"2006","unstructured":"Mark Samuel Miller . 2006 . Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation . Johns Hopkins University . Baltimore, Maryland, USA. AAI3245526 Mark Samuel Miller. 2006. Robust Composition: Towards a Unified Approach to Access Control and Concurrency Control. Ph. D. Dissertation. Johns Hopkins University. Baltimore, Maryland, USA. AAI3245526"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1352582.1352591"},{"key":"e_1_2_2_37_1","volume-title":"Hanne Riis Nielson, and Chris Hankin","author":"Nielson Flemming","year":"1999","unstructured":"Flemming Nielson , Hanne Riis Nielson, and Chris Hankin . 1999 . Type and effect systems. In Principles of Program Analysis. Springer , 283\u2013363. Flemming Nielson, Hanne Riis Nielson, and Chris Hankin. 1999. Type and effect systems. In Principles of Program Analysis. Springer, 283\u2013363."},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/3486610.3486893"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2984009"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/3136000.3136010"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1023064908962"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_7"},{"key":"e_1_2_2_44_1","volume-title":"Plotkin and Matija Pretnar","author":"Gordon","year":"2013","unstructured":"Gordon D. Plotkin and Matija Pretnar . 2013 . Handling Algebraic Effects. Logical Methods in Computer Science , 9, 4 (2013). Gordon D. Plotkin and Matija Pretnar. 2013. Handling Algebraic Effects. Logical Methods in Computer Science, 9, 4 (2013)."},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2015.12.003"},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/800194.805852"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-31057-7_13"},{"key":"e_1_2_2_48_1","volume-title":"Logic for Programming","author":"Scherer Gabriel","unstructured":"Gabriel Scherer and Jan Hoffmann . 2013. Tracking Data-Flow with Open Closure Types . In Logic for Programming , Artificial Intelligence, and Reasoning, Ken McMillan, Aart Middeldorp, and Andrei Voronkov (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 710\u2013726. isbn:978-3-642-45221-5 Gabriel Scherer and Jan Hoffmann. 2013. Tracking Data-Flow with Open Closure Types. In Logic for Programming, Artificial Intelligence, and Reasoning, Ken McMillan, Aart Middeldorp, and Andrei Voronkov (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 710\u2013726. isbn:978-3-642-45221-5"},{"key":"e_1_2_2_49_1","volume-title":"Handling Control. In Proceedings of the Conference on Programming Language Design and Implementation. ACM","author":"Sitaram Dorai","year":"1993","unstructured":"Dorai Sitaram . 1993 . Handling Control. In Proceedings of the Conference on Programming Language Design and Implementation. ACM , New York, NY, USA. 147\u2013155. Dorai Sitaram. 1993. Handling Control. In Proceedings of the Conference on Programming Language Design and Implementation. ACM, New York, NY, USA. 147\u2013155."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.2613"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1093"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408981"},{"key":"e_1_2_2_53_1","volume-title":"Proc. ACM Program. Lang., 3, POPL","author":"Zhang Yizhou","year":"2019","unstructured":"Yizhou Zhang and Andrew C. Myers . 2019. Abstraction-safe Effect Handlers via Tunneling . Proc. ACM Program. Lang., 3, POPL ( 2019 ), Article 5, Jan., 29 pages. issn:2475-1421 Yizhou Zhang and Andrew C. Myers. 2019. Abstraction-safe Effect Handlers via Tunneling. Proc. ACM Program. Lang., 3, POPL (2019), Article 5, Jan., 29 pages. issn:2475-1421"},{"key":"e_1_2_2_54_1","volume-title":"Proceedings of the Conference on Programming Language Design and Implementation. ACM","author":"Zhang Yizhou","unstructured":"Yizhou Zhang , Guido Salvaneschi , Quinn Beightol , Barbara Liskov , and Andrew C. Myers . 2016. Accepting Blame for Safe Tunneled Exceptions . In Proceedings of the Conference on Programming Language Design and Implementation. ACM , New York, NY, USA. 281\u2013295. Yizhou Zhang, Guido Salvaneschi, Quinn Beightol, Barbara Liskov, and Andrew C. Myers. 2016. Accepting Blame for Safe Tunneled Exceptions. In Proceedings of the Conference on Programming Language Design and Implementation. ACM, New York, NY, USA. 281\u2013295."},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/3428207"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/3473580"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527320","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527320","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:53Z","timestamp":1750191533000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527320"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":56,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527320"],"URL":"https:\/\/doi.org\/10.1145\/3527320","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"}}]}}