{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T23:19:00Z","timestamp":1770247140250,"version":"3.49.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"POPL","license":[{"start":{"date-parts":[[2025,1,7]],"date-time":"2025-01-07T00:00:00Z","timestamp":1736208000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nc-sa\/4.0\/"}],"funder":[{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"publisher","award":["101106046"],"award-info":[{"award-number":["101106046"]}],"id":[{"id":"10.13039\/501100000780","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":[[2025,1,7]]},"abstract":"<jats:p>In this paper, we develop and study the following perspective - just as higher-order functions give exponentials, higher-order continuations give coexponentials. From this, we design a language that combines exponentials and coexponentials, producing a duality of lambda abstraction.<\/jats:p>\n                  <jats:p>We formalise this language by giving an extension of a call-by-value simply-typed lambda-calculus with covalues, coabstraction, and coapplication. We develop the semantics of this language using the axiomatic structure of continuations, which we use to produce an equational theory, that gives a complete axiomatisation of control effects. We give a computational interpretation to this language using speculative execution and backtracking, and use this to derive the classical control operators and computational interpretation of classical logic, and encode common patterns of control flow using continuations. By dualising functional completeness, we further develop duals of first-order arrow languages using coexponentials. Finally, we discuss the implementation of this duality as control operators in programming, and develop some applications.<\/jats:p>","DOI":"10.1145\/3704848","type":"journal-article","created":{"date-parts":[[2025,1,9]],"date-time":"2025-01-09T05:48:42Z","timestamp":1736401722000},"page":"332-361","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["The Duality of \u03bb-Abstraction"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-2030-8056","authenticated-orcid":false,"given":"Vikraman","family":"Choudhury","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Bologna, Bologna, Italy"},{"name":"Inria Sophia Antipolis, Valbonne, France"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3033-9091","authenticated-orcid":false,"given":"Simon J.","family":"Gay","sequence":"additional","affiliation":[{"name":"University of Glasgow, Glasgow, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,1,9]]},"reference":[{"key":"e_1_3_2_2_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01201353"},{"key":"e_1_3_2_3_1","doi-asserted-by":"publisher","DOI":"10.1016\/0003-4843(74)90003-5"},{"key":"e_1_3_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0022493"},{"key":"e_1_3_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/800087.802799"},{"key":"e_1_3_2_6_1","first-page":"308","volume-title":"Introduction to Higher-Order Categorical Logic","author":"Lambek J.","year":"1988","unstructured":"J. Lambek and P. J. Scott. Mar. 25, 1988. Introduction to Higher-Order Categorical Logic. Cambridge University Press, (Mar. 25, 1988). 308 pp. isbn: 978-0-521-35653-4. Google Books: 6PY_emBeGjUC (cit. on p. 2)."},{"key":"e_1_3_2_7_1","first-page":"1","volume-title":"The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming","author":"Luke Ong C.-H.","year":"1988","unstructured":"C.-H. Luke Ong. 1988. The Lazy Lambda Calculus: An Investigation into the Foundations of Functional Programming. University of London, Great Britain. 1 p. Retrieved Dec. 2, 2024 from http:\/\/hdl.handle.net\/10044\/1\/47211 (cit. on p. 1)."},{"key":"e_1_3_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0018355"},{"key":"e_1_3_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_3_2_10_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_3_2_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001328"},{"key":"e_1_3_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0013061"},{"key":"e_1_3_2_13_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1993.1044"},{"key":"e_1_3_2_14_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680000085X"},{"key":"e_1_3_2_15_1","doi-asserted-by":"publisher","DOI":"10.7146\/dpb.v22i462.6935"},{"key":"e_1_3_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-57208-2_35"},{"key":"e_1_3_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"e_1_3_2_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-02880-3_8"},{"key":"e_1_3_2_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60164-3_28"},{"key":"e_1_3_2_20_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001195"},{"key":"e_1_3_2_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614964"},{"key":"e_1_3_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/263699.263722"},{"key":"e_1_3_2_23_1","article-title":"Categorical Structure of Continuation Passing Style","author":"Thielecke Hayo","year":"1997","unstructured":"Hayo Thielecke. 1997. \u201cCategorical Structure of Continuation Passing Style.\u201d The University of Edinburgh. Retrieved Jan. 6, 2023 from https:\/\/era.ed.ac.uk\/handle\/1842\/14533 (cit. on pp. 3, 8).","journal-title":"The University of Edinburgh"},{"key":"e_1_3_2_24_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796898003141"},{"key":"e_1_3_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/568547.568561"},{"key":"e_1_3_2_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/357766.351262"},{"key":"e_1_3_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(99)00124-3"},{"key":"e_1_3_2_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950100336X"},{"key":"e_1_3_2_29_1","unstructured":"Paul Blain Levy. 2001. \u201cCall-by-Push-Value.\u201d Ph.D. Dissertation. Queen Mary University of London. Retrieved June 6 2023 from https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.369233 (cit. on p. 8)."},{"key":"e_1_3_2_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950000311X"},{"key":"e_1_3_2_31_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.2001.2947"},{"issue":"12","key":"e_1_3_2_32_1","first-page":"248","article-title":"Sober Spaces and Continuations","volume":"10","author":"Taylor Paul","year":"2002","unstructured":"Paul Taylor. July 2002. \u201cSober Spaces and Continuations.\u201d Theory and Applications of Categories, 10, 12, (July 2002), 248\u2013299. PaulTaylor.EU\/ASD\/sobsc (cit. on pp. 9, 31).","journal-title":"Theory and Applications of Categories"},{"key":"e_1_3_2_33_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-007-0954-6_7"},{"key":"e_1_3_2_34_1","unstructured":"Peter Selinger. 2003. \u201cFrom Continuation Passing Style to Krivine\u2019s Abstract Machine.\u201d https:\/\/www.mscs.dal.ca\/~selinger\/papers\/krivine.pdf (cit. on p. 27)."},{"key":"e_1_3_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944723"},{"key":"e_1_3_2_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.08.001"},{"key":"e_1_3_2_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11787006_38"},{"key":"e_1_3_2_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.026"},{"key":"e_1_3_2_39_1","unstructured":"Paul-Andr\u00e9 Melli\u00e8s and Nicolas Tabareau. 2007. \u201cLinear Continuations and Duality.\u201d working paper or preprint. (2007). Retrieved Dec. 19 2022 from https:\/\/hal.archives-ouvertes.fr\/hal-00339156 (cit. on p. 31)."},{"key":"e_1_3_2_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-87531-4_13"},{"key":"e_1_3_2_41_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9006-0"},{"key":"e_1_3_2_42_1","doi-asserted-by":"publisher","DOI":"10.1017\/S095679680900728X"},{"key":"e_1_3_2_43_1","unstructured":"Noam Zeilberger. 2009. \u201cThe Logical Basis of Evaluation Order and Pattern-Matching.\u201d Ph.D. Dissertation. Carnegie Mellon University USA. 191 pp. (cit. on p. 27)."},{"key":"e_1_3_2_44_1","doi-asserted-by":"publisher","DOI":"10.4171\/088"},{"key":"e_1_3_2_45_1","first-page":"1","volume-title":"No-Cloning In Categorical Quantum Mechanics","author":"Abramsky Samson","year":"2012","unstructured":"Samson Abramsky. Mar. 19, 2012. No-Cloning In Categorical Quantum Mechanics. Comment: 35 pages. Appeared in Semantic Techniques in Quantum Computation, ed. S. Gay and I. Mackie, pages 1\u201328, Cambridge University Press 2010 Comment: 35 pages. Appeared in Semantic Techniques in Quantum Computation, ed. S. Gay and I. Mackie, pages 1-28, Cambridge University Press 2010. (Mar. 19, 2012). arXiv: 0910. 2401 [quant-ph]. Retrieved June 1, 2023 from http:\/\/arxiv.org\/abs\/0910.2401. Pre-published (cit. on pp. 2, 3)."},{"key":"e_1_3_2_46_1","doi-asserted-by":"publisher","DOI":"10.70930\/tac\/qiwseicr"},{"key":"e_1_3_2_47_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.153.3"},{"key":"e_1_3_2_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/2628136.2628160"},{"key":"e_1_3_2_49_1","doi-asserted-by":"publisher","DOI":"10.1145\/2837614.2837652"},{"key":"e_1_3_2_50_1","unstructured":"Harley Eades III and Gianluigi Bellin. Aug. 19 2017. A Cointuitionistic Adjoint Logic. Comment: 54 pages. (Aug. 19 2017). arXiv: 1708.05896 [cs]. Retrieved Jan. 3 2023 from http:\/\/arxiv.org\/abs\/1708.05896. Pre-published (cit. on pp. 2 3)."},{"key":"e_1_3_2_51_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2016.10.008"},{"key":"e_1_3_2_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408993"},{"key":"e_1_3_2_53_1","article-title":"Typed \u03bb-Calculus: Course Notes","author":"Blain Paul","year":"2021","unstructured":"Paul Blain Levy. Apr. 2021. \u201cTyped \u03bb-Calculus: Course Notes\u201d Midlands Graduate School in the Foundations of Computing Science, (Apr. 2021). https:\/\/www.cs.bham.ac.uk\/~pbl\/mgsall.pdf (cit. on p. 4).","journal-title":"Midlands Graduate School in the Foundations of Computing Science"},{"key":"e_1_3_2_54_1","doi-asserted-by":"publisher","unstructured":"[SW] Vikraman Choudhury Artifact for The Duality of \u03bb-Abstraction version v0.3.1 Oct. 30 2024. Zenodo. doi: https:\/\/doi.org\/10.5281\/ZENODO.14015102 10.5281\/ZENODO.14015102 url: https:\/\/doi.org\/10.5281\/zenodo.14015102 10.5281\/zenodo.14015102 (cit. on pp. 4 28).","DOI":"10.5281\/ZENODO.14015102"},{"key":"e_1_3_2_55_1","unstructured":"Jacob Errington. 2024. Jacob Errington | SAT Solving with Higher-Order Continuations. Retrieved Oct. 26 2024 from https:\/\/jerrington.me\/posts\/2022-10-22-higher-order-continuations.html (cit. on p. 25)."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704848","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3704848","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T10:15:06Z","timestamp":1770200106000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3704848"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,1,7]]},"references-count":54,"journal-issue":{"issue":"POPL","published-print":{"date-parts":[[2025,1,7]]}},"alternative-id":["10.1145\/3704848"],"URL":"https:\/\/doi.org\/10.1145\/3704848","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,1,7]]},"assertion":[{"value":"2024-07-11","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-11-07","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-01-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}