Creative Commons Attribution 4.0 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: https://drops.dagstuhl.de/opus/volltexte/2021/14250/
Cong, Youyou ; Ishio, Chiaki ; Honda, Kaho ; Asai, Kenichi
A Functional Abstraction of Typed Invocation Contexts
| pdf-format: |
|
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}
}
| Keywords: | delimited continuations, control operators, control and prompt, CPS translation, type system | |
| Seminar: | 6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021) | |
| Issue date: | 2021 | |
| Date of publication: | 06.07.2021 | |
| Supplementary Material: | Model (Agda Formalization): https://github.com/YouyouCong/fscd21-artifact archived at: https://archive.softwareheritage.org/swh:1:dir:9eaf9840fc9b223e030f633c3f9b3b5ea7b47bc6 |
