{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,9]],"date-time":"2026-01-09T03:05:13Z","timestamp":1767927913147,"version":"3.49.0"},"reference-count":40,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2020,8,2]],"date-time":"2020-08-02T00:00:00Z","timestamp":1596326400000},"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":[[2020,8,2]]},"abstract":"<jats:p>\n            In this paper, we take a pervasively effectful (in the style of ML) typed lambda calculus, and show how to\n            <jats:italic>extend<\/jats:italic>\n            it to permit capturing pure expressions with types. Our key observation is that, just as the pure simply-typed lambda calculus can be extended to support effects with a monadic type discipline, an impure typed lambda calculus can be extended to support purity with a\n            <jats:italic>comonadic<\/jats:italic>\n            type discipline.\n          <\/jats:p>\n          <jats:p>\n            We establish the correctness of our type system via a simple denotational model, which we call the\n            <jats:italic>capability space<\/jats:italic>\n            model. Our model formalises the intuition common to systems programmers that the ability to perform effects should be controlled via access to a permission or capability, and that a program is\n            <jats:italic>capability-safe<\/jats:italic>\n            if it performs no effects that it does not have a runtime capability for. We then identify the axiomatic categorical structure that the capability space model validates, and use these axioms to give a categorical semantics for our comonadic type system. We then give an equational theory (substitution and the call-by-value \u03b2 and \u03b7 laws) for the imperative lambda calculus, and show its soundness relative to this semantics.\n          <\/jats:p>\n          <jats:p>Finally, we give a translation of the pure simply-typed lambda calculus into our comonadic imperative calculus, and show that any two terms which are \u03b2\u03b7-equal in the STLC are equal in the equational theory of the comonadic calculus, establishing that pure programs can be mapped in an equation-preserving way into our imperative calculus.<\/jats:p>","DOI":"10.1145\/3408993","type":"journal-article","created":{"date-parts":[[2020,8,3]],"date-time":"2020-08-03T13:48:02Z","timestamp":1596462482000},"page":"1-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":9,"title":["Recovering purity with comonads and capabilities"],"prefix":"10.1145","volume":"4","author":[{"given":"Vikraman","family":"Choudhury","sequence":"first","affiliation":[{"name":"Indiana University, USA \/ University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Neel","family":"Krishnaswami","sequence":"additional","affiliation":[{"name":"University of Cambridge, UK"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,8,3]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44802-0_21"},{"key":"e_1_2_2_2_1","volume-title":"O'Hearn","author":"Berdine Josh","year":"2006"},{"key":"e_1_2_2_3_1","volume-title":"Programming Languages and Systems","author":"Brunel Alo\u00efs"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-89366-2_14"},{"key":"e_1_2_2_5_1","volume-title":"'99","author":"Crary Karl","year":"1999"},{"key":"e_1_2_2_6_1","volume-title":"RevisitTeydp. eIdnLambda Calculi and Applications, Pierre-Louis Curien (Ed.)","author":"Lago Ugo Dal"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.111105C6harleston,SouthCarolina,USA."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/365230.365252"},{"key":"e_1_2_2_9_1","volume-title":"Giuseppe Castagna (Ed.)","author":"Dodds Mike"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-47797-7_5"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/319838.319848"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90045-4"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2822-6_8"},{"key":"e_1_2_2_14_1","doi-asserted-by":"publisher","DOI":"10.1016\/s0890-5401(03)00009-9"},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(96)00169-7"},{"key":"e_1_2_2_16_1","doi-asserted-by":"crossref","unstructured":"Neelakantan R. Krishnaswami. 2013. Higher-Order Reactive Programming without Spacetime LInetaekrnsa. tIinonal Conference on Functional Programming (ICFP).  Neelakantan R. Krishnaswami. 2013. Higher-Order Reactive Programming without Spacetime LInetaekrnsa. tIinonal Conference on Functional Programming (ICFP).","DOI":"10.1145\/2500365.2500588"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/850657.850658"},{"key":"e_1_2_2_18_1","volume-title":"Capability-based computer systems","author":"Levy Henry M"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1109\/SP.2010.16"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.2307\/2268135"},{"key":"e_1_2_2_22_1","volume-title":"NDSS 2010","author":"Metler Adrian","year":"2010"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_2_26_1","volume-title":"Pawe\u0142 Urzyczyn (Ed.)","author":"Morriset Greg"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-48092-7_6"},{"key":"e_1_2_2_28_1","volume-title":"Pym","author":"O'Hearn Peter W.","year":"1999"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341714"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500000311"},{"key":"e_1_2_2_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129501003322"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/512760.512766event-place:Tucson,Arizona."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2002.1029817"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002943"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01806033"},{"key":"e_1_2_2_37_1","volume-title":"17th International Conference, CONCUR 2006, Bonn, Germany, August 27-30, 2006, Proceedings (Lecture Notes in Computer Science), Christel Baier and Holger Hermanns (Eds.)","volume":"4137","author":"Terauchi Tachio","year":"2006"},{"key":"e_1_2_2_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00153-007-0042-6"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90147-a"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289429"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/355616.364017"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408993","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3408993","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:59Z","timestamp":1750193279000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3408993"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,2]]},"references-count":40,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2020,8,2]]}},"alternative-id":["10.1145\/3408993"],"URL":"https:\/\/doi.org\/10.1145\/3408993","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,8,2]]},"assertion":[{"value":"2020-08-03","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}