文章基本信息

标题：A Reflection on Continuation-Composing Style
本地全文：下载
作者：Dariusz Biernacki ; Mateusz Pyzik ; Filip Sieczkowski 等
期刊名称：LIPIcs : Leibniz International Proceedings in Informatics
电子版ISSN：1868-8969
出版年度：2020
卷号：167
页码：18:1-18:17
DOI：10.4230/LIPIcs.FSCD.2020.18
出版社：Schloss Dagstuhl -- Leibniz-Zentrum fuer Informatik
摘要：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.
关键词：delimited control; continuation-passing style; reflection; call-by-value lambda calculus; computational lambda calculus