2026-07-23T18:08:53Z https://drops.dagstuhl.de/oai

oai:drops-oai.dagstuhl.de:12340 2024-03-06T10:50:00Z ddc:004 open_access

A Reflection on Continuation-Composing Style Biernacki, Dariusz Pyzik, Mateusz Sieczkowski, Filip delimited control continuation-passing style reflection call-by-value lambda calculus computational lambda calculus We present a study of the continuation-composing style (CCS) that describes the image of the CPS translation of Danvy and Filinski’s shift and reset delimited-control operators. In CCS continuations are composable rather than abortive as in the traditional CPS, and, therefore, the structure of terms is considerably more complex. We show that the CPS translation from Moggi’s computational lambda calculus extended with shift and reset has a right inverse and that the two translations form a reflection i.e., a Galois connection in which the target is isomorphic to a subset of the source (the orders are given by the reduction relations). Furthermore, we use this result to show that Plotkin’s call-by-value lambda calculus extended with shift and reset is isomorphic to the image of the CPS translation. This result, in particular, provides a first direct-style transformation for delimited continuations that is an inverse of the CPS transformation up to syntactic identity. Schloss Dagstuhl – Leibniz-Zentrum für Informatik Dariusz Biernacki and Mateusz Pyzik and Filip Sieczkowski 2020 Is Part Of LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) InProceedings Text doc-type:ResearchArticle publishedVersion application/pdf doi:10.4230/LIPIcs.FSCD.2020.18 urn:nbn:de:0030-drops-123402 https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.18 eng https://creativecommons.org/licenses/by/3.0/legalcode