The Logical Essence of Compiling with Continuations
| Autor: | Espírito Santo, José, Mendes, Filipa |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2023 |
| Předmět: | |
| DOI: | 10.4230/lipics.fscd.2023.19 |
| Popis: | 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. LIPIcs, Vol. 260, 8th International Conference on Formal Structures for Computation and Deduction (FSCD 2023), pages 19:1-19:21 |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|