Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/62978
Título: | Modal embeddings and calling paradigms |
Autor(es): | Espírito Santo, José Pinto, Luís F. Uustalu, Tarmo |
Palavras-chave: | Intuitionistic S4 Call-by-name Call-by-value Comonadic lambda-calculus Standardization Indifference property |
Data: | 2019 |
Editora: | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
Revista: | Leibniz International Proceedings in Informatics, LIPIcs |
Citação: | 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. |
Resumo(s): | 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. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/62978 |
ISBN: | 978-3-95977-107-8 |
DOI: | 10.4230/LIPIcs.FSCD.2019.18 |
ISSN: | 1868-8969 |
Versão da editora: | https://drops.dagstuhl.de/opus/volltexte/2019/10525/ |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
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