Creative Commons Attribution 3.0 Unported license (CC-BY 3.0)when quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2020.18
URN: urn:nbn:de:0030-drops-123402
URL: https://drops.dagstuhl.de/opus/volltexte/2020/12340/
Biernacki, Dariusz ; Pyzik, Mateusz ; Sieczkowski, Filip
A Reflection on Continuation-Composing Style
| pdf-format: |
|
Abstract
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.
BibTeX - Entry
@InProceedings{biernacki_et_al:LIPIcs:2020:12340,
author = {Dariusz Biernacki and Mateusz Pyzik and Filip Sieczkowski},
title = {{A Reflection on Continuation-Composing Style}},
booktitle = {5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)},
pages = {18:1--18:17},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-155-9},
ISSN = {1868-8969},
year = {2020},
volume = {167},
editor = {Zena M. Ariola},
publisher = {Schloss Dagstuhl--Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2020/12340},
URN = {urn:nbn:de:0030-drops-123402},
doi = {10.4230/LIPIcs.FSCD.2020.18},
annote = {Keywords: delimited control, continuation-passing style, reflection, call-by-value lambda calculus, computational lambda calculus}
}
| Keywords: | delimited control, continuation-passing style, reflection, call-by-value lambda calculus, computational lambda calculus | |
| Seminar: | 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020) | |
| Issue date: | 2020 | |
| Date of publication: | 28.06.2020 |
