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.2023.19
URN: urn:nbn:de:0030-drops-180036
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18003/
Espírito Santo, José ;
Mendes, Filipa
The Logical Essence of Compiling with Continuations
Abstract
The essence of compiling with continuations is that conversion to continuation-passing style (CPS) is equivalent to a source language transformation converting to administrative normal form (ANF). Taking as source language Moggi’s computational lambda-calculus (λ{?}), we define an alternative to the CPS-translation with target in the sequent calculus LJQ, named value-filling style (VFS) translation, and making use of the ability of the sequent calculus to represent contexts formally. The VFS-translation requires no type translation: indeed, double negations are introduced only when encoding the VFS target language in the CPS target language. This optional encoding, when composed with the VFS-translation reconstructs the original CPS-translation. Going back to direct style, the "essence" of the VFS-translation is that it reveals a new sublanguage of ANF, the value-enclosed style (VES), next to another one, the continuation-enclosing style (CES): such an alternative is due to a dilemma in the syntax of λ{?}, concerning how to expand the application constructor. In the typed scenario, VES and CES correspond to an alternative between two proof systems for call-by-value, LJQ and natural deduction with generalized applications, confirming proof theory as a foundation for intermediate representations.
BibTeX - Entry
@InProceedings{espiritosanto_et_al:LIPIcs.FSCD.2023.19,
author = {Esp{\'\i}rito Santo, Jos\'{e} and Mendes, Filipa},
title = {{The Logical Essence of Compiling with Continuations}},
booktitle = {8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023)},
pages = {19:1--19:21},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-277-8},
ISSN = {1868-8969},
year = {2023},
volume = {260},
editor = {Gaboardi, Marco and van Raamsdonk, Femke},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18003},
URN = {urn:nbn:de:0030-drops-180036},
doi = {10.4230/LIPIcs.FSCD.2023.19},
annote = {Keywords: Continuation-passing style, Sequent calculus, Generalized applications, Administrative normal form}
}
|
Keywords: |
|
Continuation-passing style, Sequent calculus, Generalized applications, Administrative normal form |
|
Collection: |
|
8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
28.06.2023 |
