License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.FSCD.2021.12
URN: urn:nbn:de:0030-drops-142507
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14250/
Cong, Youyou ;
Ishio, Chiaki ;
Honda, Kaho ;
Asai, Kenichi
A Functional Abstraction of Typed Invocation Contexts
Abstract
In their paper "A Functional Abstraction of Typed Contexts", Danvy and Filinski show how to derive a type system of the shift and reset operators from a CPS translation. In this paper, we show how this method scales to Felleisen’s control and prompt operators. Compared to shift and reset, control and prompt exhibit a more dynamic behavior, in that they can manipulate a trail of contexts surrounding the invocation of captured continuations. Our key observation is that, by adopting a functional representation of trails in the CPS translation, we can derive a type system that allows fine-grain reasoning of programs involving manipulation of invocation contexts.
BibTeX - Entry
@InProceedings{cong_et_al:LIPIcs.FSCD.2021.12,
author = {Cong, Youyou and Ishio, Chiaki and Honda, Kaho and Asai, Kenichi},
title = {{A Functional Abstraction of Typed Invocation Contexts}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {12:1--12:18},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-191-7},
ISSN = {1868-8969},
year = {2021},
volume = {195},
editor = {Kobayashi, Naoki},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/14250},
URN = {urn:nbn:de:0030-drops-142507},
doi = {10.4230/LIPIcs.FSCD.2021.12},
annote = {Keywords: delimited continuations, control operators, control and prompt, CPS translation, type system}
}
