DROPS

Document

DOI: 10.4230/LIPIcs.FSCD.2020.18

A Reflection on Continuation-Composing Style

Authors: Dariusz Biernacki, Mateusz Pyzik, and Filip Sieczkowski

Published in: LIPIcs, Volume 167, 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020)

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.

Cite as

Dariusz Biernacki, Mateusz Pyzik, and Filip Sieczkowski. A Reflection on Continuation-Composing Style. In 5th International Conference on Formal Structures for Computation and Deduction (FSCD 2020). Leibniz International Proceedings in Informatics (LIPIcs), Volume 167, pp. 18:1-18:17, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2020)

Copy BibTex To Clipboard

@InProceedings{biernacki_et_al:LIPIcs.FSCD.2020.18,
  author =	{Biernacki, Dariusz and Pyzik, Mateusz and Sieczkowski, Filip},
  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 =	{Ariola, Zena M.},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.FSCD.2020.18},
  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}
}

Search Results

Documents authored by Pyzik, Mateusz

A Reflection on Continuation-Composing Style

Abstract

Cite as

Thanks for your feedback!

Could not send message