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.16
URN: urn:nbn:de:0030-drops-142547
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14254/
Fujii, Maika ;
Asai, Kenichi
Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators
Abstract
This paper derives an abstract machine and a virtual machine for the λ-calculus with four variants of delimited-control operators: shift/reset, control/prompt, shift₀/reset₀, and control₀/prompt₀. Starting from Shan’s definitional interpreter for the four operators, we successively apply various meaning-preserving transformations. Both trails of invocation contexts (needed for control and control₀) and metacontinuations (needed for shift₀ and control₀) are defunctionalized and eventually represented as a list of stack frames. The resulting virtual machine clearly models not only how the control operators and captured continuations behave but also when and which portion of stack frames is copied to the heap.
BibTeX - Entry
@InProceedings{fujii_et_al:LIPIcs.FSCD.2021.16,
author = {Fujii, Maika and Asai, Kenichi},
title = {{Derivation of a Virtual Machine For Four Variants of Delimited-Control Operators}},
booktitle = {6th International Conference on Formal Structures for Computation and Deduction (FSCD 2021)},
pages = {16:1--16:19},
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/14254},
URN = {urn:nbn:de:0030-drops-142547},
doi = {10.4230/LIPIcs.FSCD.2021.16},
annote = {Keywords: delimited-control operators, functional derivation, CPS transformation, defunctionalization, abstract machine, virtual machine}
}
