Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/62978
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | por |
dc.contributor.author | Pinto, Luís F. | por |
dc.contributor.author | Uustalu, Tarmo | por |
dc.date.accessioned | 2020-01-07T11:13:25Z | - |
dc.date.available | 2020-01-07T11:13:25Z | - |
dc.date.issued | 2019 | - |
dc.identifier.citation | Espírito Santo, J., Pinto, L., & Uustalu, T. (2019). Modal Embeddings and Calling Paradigms. In 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019). Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. | por |
dc.identifier.isbn | 978-3-95977-107-8 | por |
dc.identifier.issn | 1868-8969 | por |
dc.identifier.uri | https://hdl.handle.net/1822/62978 | - |
dc.description.abstract | We study the computational interpretation of the two standard modal embeddings, usually named after Girard and Gödel, of intuitionistic logic into IS4. As source system we take either the call-byname (cbn) or the call-by-value (cbv) lambda-calculus with simple types. The target system can be taken to be the, arguably, simplest fragment of IS4, here recast as a very simple lambda-calculus equipped with an indeterminate lax monoidal comonad. A slight refinement of the target and of the embeddings shows that: the target is a calculus indifferent to the calling paradigms cbn/cbv, obeying a new paradigm that we baptize call-by-box (cbb), and enjoying standardization; and that Girard’s (resp. Gödel’s) embbedding is a translation of cbn (resp. cbv) lambda-calculus into this calculus, using a compilation technique we call protecting-by-a-box, enjoying the preservation and reflection properties known for cps translations - but in a stronger form that allows the extraction of standardization for cbn or cbv as consequence of standardization for cbb. The modal target and embeddings achieve thus an unification of call-by-name and call-by-value as call-by-box. | por |
dc.description.sponsorship | J.E.S. and L.P. were supported by Fundação para a Ciência e a Tecnologia (FCT) throughproject UID/MAT/00013/2013. T.U. was supported by the Estonian Ministry of Education and Research through institutional research grant IUT33-13. All three authors received support fromthe COST action CA15123 EUTYPES. | por |
dc.language.iso | eng | por |
dc.publisher | Schloss Dagstuhl - Leibniz-Zentrum für Informatik | por |
dc.relation | info:eu-repo/grantAgreement/FCT/5876/147370/PT | por |
dc.rights | openAccess | por |
dc.rights.uri | http://creativecommons.org/licenses/by/4.0/ | por |
dc.subject | Intuitionistic S4 | por |
dc.subject | Call-by-name | por |
dc.subject | Call-by-value | por |
dc.subject | Comonadic lambda-calculus | por |
dc.subject | Standardization | por |
dc.subject | Indifference property | por |
dc.title | Modal embeddings and calling paradigms | por |
dc.type | conferencePaper | por |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | https://drops.dagstuhl.de/opus/volltexte/2019/10525/ | por |
oaire.citationConferenceDate | 24 Jun. - 30 Jun. 2019 | por |
sdum.event.title | 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) | por |
sdum.event.type | conference | por |
oaire.citationStartPage | 18:1 | por |
oaire.citationEndPage | 18:20 | por |
oaire.citationConferencePlace | Dortmund, Alemanha | por |
oaire.citationVolume | 131 | por |
dc.identifier.doi | 10.4230/LIPIcs.FSCD.2019.18 | por |
dc.subject.fos | Ciências Naturais::Matemáticas | por |
dc.subject.fos | Ciências Naturais::Ciências da Computação e da Informação | por |
sdum.journal | Leibniz International Proceedings in Informatics, LIPIcs | por |
sdum.conferencePublication | 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019) | por |
oaire.version | VoR | por |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
LIPIcs-FSCD-2019-18(ThePublishedVersion).pdf | 564,05 kB | Adobe PDF | Ver/Abrir |
Este trabalho está licenciado sob uma Licença Creative Commons