{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,17]],"date-time":"2026-07-17T02:25:34Z","timestamp":1784255134361,"version":"3.55.0"},"reference-count":32,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T00:00:00Z","timestamp":1680739200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by-nd\/4.0\/"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2023,4,6]]},"abstract":"<jats:p>Translating programs into continuation-passing style is a well-studied  \ntool to explicitly deal with the control structure of programs. This is  \nuseful, for example, for compilation.  \nIn a typed setting, there also is a logical interpretation of such a translation  \nas an embedding of classical logic into intuitionistic logic.  \nA naturally arising question is whether there is an inverse translation  \nback to direct style. The answer to this question depends on how the  \ncontinuation-passing translation is defined and on the domain of the inverse translation.  \nIn general, translating programs from continuation-passing style back to direct  \nstyle requires the use of control operators to account for the use of  \ncontinuations in non-trivial ways.<\/jats:p>\n          <jats:p>We present two languages, one in direct style and one in continuation-passing  \nstyle. Both languages are typed and equipped with an abstract machine semantics.  \nMoreover, both languages allow for non-trivial control flow.  \nWe further present a translation to continuation-passing style and a translation  \nback to direct style. We show that both translations are type-preserving and  \nalso preserve semantics in a very precise way giving an operational  \ncorrespondence between the two languages.  \nMoreover, we show that the compositions of the translations are well-behaved.  \nIn particular, they are syntactic one-sided inverses on the full language and full  \nsyntactic inverses when restricted to trivial control flow.<\/jats:p>","DOI":"10.1145\/3586056","type":"journal-article","created":{"date-parts":[[2023,4,6]],"date-time":"2023-04-06T21:06:02Z","timestamp":1680815162000},"page":"848-875","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":4,"title":["Back to Direct Style: Typed and Tight"],"prefix":"10.1145","volume":"7","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0260-6298","authenticated-orcid":false,"given":"Marius","family":"M\u00fcller","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-9128-0391","authenticated-orcid":false,"given":"Jonathan Immanuel","family":"Brachth\u00e4user","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-5294-5506","authenticated-orcid":false,"given":"Klaus","family":"Ostermann","sequence":"additional","affiliation":[{"name":"University of T\u00fcbingen, Germany"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2023,4,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511609619"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/2003476.2003498"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.FSCD.2020.18"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/3479394.3479399"},{"key":"e_1_2_1_5_1","volume-title":"Idris 2: Quantitative Type Theory in Action","author":"Brady Edwin","unstructured":"Edwin Brady . 2020. Idris 2: Quantitative Type Theory in Action . University of St Andrews , Scotland, UK . https:\/\/www.type-driven.org.uk\/edwinb\/papers\/idris2.pdf Edwin Brady. 2020. Idris 2: Quantitative Type Theory in Action. University of St Andrews, Scotland, UK. https:\/\/www.type-driven.org.uk\/edwinb\/papers\/idris2.pdf"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/3341643"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55253-7_8"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141564"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00733-8"},{"key":"e_1_2_1_10_1","volume-title":"The Occurrence of Continuation Parameters in CPS Terms. Department of Computer Science","author":"Danvy Olivier","unstructured":"Olivier Danvy and Frank Pfenning . 1995. The Occurrence of Continuation Parameters in CPS Terms. Department of Computer Science , Carnegie Mellon University . Olivier Danvy and Frank Pfenning. 1995. The Occurrence of Continuation Parameters in CPS Terms. Department of Computer Science, Carnegie Mellon University."},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3385994"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(87)90109-5"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1145\/155090.155113"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/96709.96714"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/174675.178053"},{"key":"e_1_2_1_16_1","first-page":"479","article-title":"The Formulae-as-Types Notion of Construction. To H.B. Curry: Essays on Combinatory Logic","volume":"44","author":"Howard William A","year":"1980","unstructured":"William A Howard . 1980 . The Formulae-as-Types Notion of Construction. To H.B. Curry: Essays on Combinatory Logic , Lambda Calculus and Formalism , 44 (1980), 479 \u2013 490 . William A Howard. 1980. The Formulae-as-Types Notion of Construction. To H.B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, 44 (1980), 479\u2013490.","journal-title":"Lambda Calculus and Formalism"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10990-007-9009-x"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/944705.944722"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1291151.1291179"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-73228-0_17"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/158511.158613"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00088-9"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-35182-2_21"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1145\/3062341.3062380"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1989.39155"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90052-4"},{"key":"e_1_2_1_27_1","volume-title":"Jonathan Immanuel Brachth\u00e4user, and Klaus Ostermann","author":"M\u00fcller Marius","year":"2023","unstructured":"Marius M\u00fcller , Philipp Schuster , Jonathan Immanuel Brachth\u00e4user, and Klaus Ostermann . 2023 . Back to Direct Style : Typed and Tight. University of T\u00fcbingen , Germany. https:\/\/se.informatik.uni-tuebingen.de\/publications\/mueller23continuation Marius M\u00fcller, Philipp Schuster, Jonathan Immanuel Brachth\u00e4user, and Klaus Ostermann. 2023. Back to Direct Style: Typed and Tight. University of T\u00fcbingen, Germany. https:\/\/se.informatik.uni-tuebingen.de\/publications\/mueller23continuation"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.7146\/brics.v9i2.21719"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/141471.141563"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01019462"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/267959.269968"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/3408975"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586056","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3586056","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T18:08:10Z","timestamp":1750183690000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3586056"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,4,6]]},"references-count":32,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2023,4,6]]}},"alternative-id":["10.1145\/3586056"],"URL":"https:\/\/doi.org\/10.1145\/3586056","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2023,4,6]]},"assertion":[{"value":"2023-04-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}