{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T21:09:58Z","timestamp":1770239398646,"version":"3.49.0"},"reference-count":52,"publisher":"Association for Computing Machinery (ACM)","issue":"ICFP","license":[{"start":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T00:00:00Z","timestamp":1723680000000},"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":[[2024,8,15]]},"abstract":"<jats:p>The continuation-passing style translation often employed by compilers gives rise to a class of intermediate representation languages where functions are not allowed to return anymore. Though the primary use of these intermediate representation languages is to expose details about a program\u2019s control flow, they may be equipped with an equational theory in order to be seen as specialized calculi, which in turn may be related to the original languages by means of a factorization theorem. In this paper, we explore Thielecke\u2019s CPS-calculus, a small theory of continuations inspired by compiler implementations, and study its metatheory. We extend it with a sound reduction semantics that faithfully represents optimization rules used in actual compilers, and prove that it acts as a suitable theoretical foundation for the intermediate representation of Appel\u2019s and Kennedy\u2019s compilers by following the guidelines set out by Plotkin. Finally, we prove that the CPS-calculus is strongly normalizing in the simply typed setting by using a novel proof method for reasoning about reducibility at a distance, from which logical consistency follows. Taken together, these results close a gap in the existing literature, providing a formal theory for reasoning about intermediate representations.<\/jats:p>","DOI":"10.1145\/3674630","type":"journal-article","created":{"date-parts":[[2024,8,15]],"date-time":"2024-08-15T12:49:04Z","timestamp":1723726144000},"page":"147-176","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["On the Operational Theory of the CPS-Calculus: Towards a Theoretical Foundation for IRs"],"prefix":"10.1145","volume":"8","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-3838-652X","authenticated-orcid":false,"given":"Paulo","family":"Torrens","sequence":"first","affiliation":[{"name":"University of Kent, Canterbury, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-7058-7842","authenticated-orcid":false,"given":"Dominic","family":"Orchard","sequence":"additional","affiliation":[{"name":"University of Kent, Canterbury, United Kingdom"},{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7581-4146","authenticated-orcid":false,"given":"Cristiano","family":"Vasconcellos","sequence":"additional","affiliation":[{"name":"Santa Catarina State University, Joinville, Brazil"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2024,8,15]]},"reference":[{"key":"e_1_3_1_2_1","first-page":"65","volume-title":"The Lazy Lambda Calculus","author":"Abramsky Samson","year":"1990","unstructured":"Samson Abramsky. 1990. The Lazy Lambda Calculus. Addison-Wesley Longman Publishing Co., Inc., USA, 65\u2013116."},{"key":"e_1_3_1_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.RTA.2013.39"},{"key":"e_1_3_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3531130.3532445"},{"key":"e_1_3_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/2578855.2535886"},{"key":"e_1_3_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-34175-6_9"},{"key":"e_1_3_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15205-4_30"},{"key":"e_1_3_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/2034574.2034830"},{"key":"e_1_3_1_9_1","unstructured":"Roberto M. Amadio. 2017. Operational methods in semantics (lecture notes). https:\/\/api.semanticscholar.org\/CorpusID:67205591 Accessed on June 2024."},{"key":"e_1_3_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-32495-6_5"},{"key":"e_1_3_1_11_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609619"},{"key":"e_1_3_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/278283.278285"},{"key":"e_1_3_1_13_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002839"},{"key":"e_1_3_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/199448.199507"},{"key":"e_1_3_1_15_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274112"},{"key":"e_1_3_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3131851.3131859"},{"key":"e_1_3_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/11431664_9"},{"key":"e_1_3_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/289423.289435"},{"key":"e_1_3_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/3158110"},{"key":"e_1_3_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341643"},{"key":"e_1_3_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/115372.115320"},{"key":"e_1_3_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80281-6"},{"key":"e_1_3_1_23_1","doi-asserted-by":"crossref","unstructured":"Olivier Danvy and Julia Lawall. 1996. Back to Direct Style II: First-Class Continuations. BRICS Report Series RS-96-20 (1996).","DOI":"10.7146\/brics.v3i20.19982"},{"key":"e_1_3_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_3_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.08.001"},{"key":"e_1_3_1_26_1","doi-asserted-by":"publisher","DOI":"10.2307\/2274726"},{"key":"e_1_3_1_27_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_3_1_28_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0956796897002748"},{"key":"e_1_3_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2010.01.028"},{"key":"e_1_3_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/202529.202532"},{"key":"e_1_3_1_31_1","unstructured":"Andrew Kennedy. 2005. [TYPES] normalization and programming languages. http:\/\/lists.seas.upenn.edu\/pipermail\/typeslist\/2005\/000970.html Sent to the [TYPES] mailing list. Accessed on July 11th 2023."},{"key":"e_1_3_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291179"},{"key":"e_1_3_1_33_1","volume-title":"Call-by-push-value. Ph. D. Dissertation","author":"Levy Paul Blain","year":"2001","unstructured":"Paul Blain Levy. 2001. Call-by-push-value. Ph. D. Dissertation. Queen Mary University of London, UK. https:\/\/ethos.bl.uk\/OrderDetails.do?uin=uk.bl.ethos.369233"},{"key":"e_1_3_1_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062380"},{"key":"e_1_3_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/s00236-009-0112-9"},{"key":"e_1_3_1_36_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129504004323"},{"key":"e_1_3_1_37_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500001407"},{"key":"e_1_3_1_38_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55719-9_114"},{"key":"e_1_3_1_39_1","doi-asserted-by":"publisher","DOI":"10.1145\/319301.319345"},{"key":"e_1_3_1_40_1","doi-asserted-by":"publisher","DOI":"10.48550\/arXiv.2001.11334"},{"key":"e_1_3_1_41_1","doi-asserted-by":"publisher","DOI":"10.1017\/S096012950007002X"},{"key":"e_1_3_1_42_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(75)90017-1"},{"key":"e_1_3_1_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019459"},{"key":"e_1_3_1_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/141478.141563"},{"key":"e_1_3_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/267959.269968"},{"key":"e_1_3_1_46_1","doi-asserted-by":"publisher","DOI":"10.2178\/bsl\/1182353926"},{"key":"e_1_3_1_47_1","doi-asserted-by":"publisher","DOI":"10.5555\/889478"},{"key":"e_1_3_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(89)80045-8"},{"key":"e_1_3_1_49_1","volume-title":"Categorical Structure of Continuation Passing Style. Ph. D. Dissertation","author":"Thielecke Hayo","year":"1997","unstructured":"Hayo Thielecke. 1997a. Categorical Structure of Continuation Passing Style. Ph. D. Dissertation. University of Edinburgh."},{"key":"e_1_3_1_50_1","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80149-5"},{"key":"e_1_3_1_51_1","doi-asserted-by":"publisher","unstructured":"Paulo Torrens. 2024. Artifact for \u201cOn the Operational Theory of the CPS-calculus\u201d. https:\/\/doi.org\/10.5281\/zenodo.11498450 10.5281\/zenodo.11498450","DOI":"10.5281\/zenodo.11498450"},{"key":"e_1_3_1_52_1","doi-asserted-by":"publisher","DOI":"10.1145\/944746.944723"},{"key":"e_1_3_1_53_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2003.08.004"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674630","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3674630","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,2,4]],"date-time":"2026-02-04T07:50:18Z","timestamp":1770191418000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3674630"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024,8,15]]},"references-count":52,"journal-issue":{"issue":"ICFP","published-print":{"date-parts":[[2024,8,15]]}},"alternative-id":["10.1145\/3674630"],"URL":"https:\/\/doi.org\/10.1145\/3674630","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2024,8,15]]},"assertion":[{"value":"2024-02-28","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-06-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2024-08-15","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}