Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/87946
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | por |
dc.contributor.author | Mendes, Filipa | por |
dc.date.accessioned | 2024-01-08T10:38:25Z | - |
dc.date.available | 2024-01-08T10:38:25Z | - |
dc.date.issued | 2023 | - |
dc.identifier.isbn | 978-3-95977-277-8 | por |
dc.identifier.issn | 1868-8969 | por |
dc.identifier.uri | https://hdl.handle.net/1822/87946 | - |
dc.description.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 (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. | por |
dc.description.sponsorship | FCT -Fundação para a Ciência e a Tecnologia(UIDB/00013/2020) | por |
dc.language.iso | eng | por |
dc.publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik | por |
dc.relation | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDB%2F00013%2F2020/PT | por |
dc.relation | info:eu-repo/grantAgreement/FCT/6817 - DCRRNI ID/UIDP%2F00013%2F2020/PT | por |
dc.rights | openAccess | por |
dc.rights.uri | http://creativecommons.org/licenses/by/4.0/ | por |
dc.subject | Continuation-passing style | por |
dc.subject | Sequent calculus | por |
dc.subject | Generalized applications | por |
dc.subject | Administrative normal form | por |
dc.title | The logical essence of compiling with continuations | por |
dc.type | conferencePaper | por |
dc.peerreviewed | yes | por |
oaire.citationConferenceDate | 03 - 06 Jul. 2023 | por |
sdum.event.title | 8th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2023 | por |
sdum.event.type | conference | por |
oaire.citationConferencePlace | Roma | por |
oaire.citationVolume | 260 | por |
dc.identifier.doi | 10.4230/LIPIcs.FSCD.2023.19 | por |
dc.subject.fos | Ciências Naturais::Matemáticas | por |
sdum.journal | Leibniz International Proceedings in Informatics, LIPIcs | por |
sdum.conferencePublication | 8th International Conference on Formal Structures for Computation and Deduction, {FSCD} 2023, July 3-6, 2023, Rome, Italy | por |
oaire.version | VoR | por |
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