Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/87946
Título: | The logical essence of compiling with continuations |
Autor(es): | Espírito Santo, José Mendes, Filipa |
Palavras-chave: | Continuation-passing style Sequent calculus Generalized applications Administrative normal form |
Data: | 2023 |
Editora: | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
Revista: | Leibniz International Proceedings in Informatics, LIPIcs |
Resumo(s): | 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 (lambdaC), 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 lambdaC, 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. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/87946 |
ISBN: | 978-3-95977-277-8 |
DOI: | 10.4230/LIPIcs.FSCD.2023.19 |
ISSN: | 1868-8969 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
main-proceedings.pdf | 784,55 kB | Adobe PDF | Ver/Abrir |
Este trabalho está licenciado sob uma Licença Creative Commons