Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/87619| Título: | Plotkin's call-by-value λ-calculus as a modal calculus |
| Autor(es): | Espírito Santo, José Pinto, Luís F. Uustalu, Tarmo |
| Palavras-chave: | Call-by-name Call-by-value Girard's embedding Gödel's embedding S4 modal logic λ-calculus lambda-calculus Godel's embedding |
| Data: | Jan-2022 |
| Editora: | Elsevier 1 |
| Revista: | Journal of Logical and Algebraic Methods in Programming |
| Citação: | Espírito Santo, J., Pinto, L., & Uustalu, T. (2022, June). Plotkin's call-by-value λ-calculus as a modal calculus. Journal of Logical and Algebraic Methods in Programming. Elsevier BV. http://doi.org/10.1016/j.jlamp.2022.100775 |
| Resumo(s): | In the authors' previous analysis of the calling paradigms call-by-name and call-by-value through Girard's and Gödel's embeddings into the S4 modal logic, an asymmetry remains: the two paradigms are unified by the call-by-box paradigm of the modal target, but only for call-by-name can one say that the paradigm exists, up to isomorphism, inside the modal target. In this paper, we show that, by pushing further the modal analysis, a symmetric situation is revealed, in that ordinary and Plotkin's λ-calculi are shown to truly co-exist inside a simple modal calculus. |
| Tipo: | Artigo |
| URI: | https://hdl.handle.net/1822/87619 |
| DOI: | 10.1016/j.jlamp.2022.100775 |
| ISSN: | 2352-2208 |
| e-ISSN: | 2352-2216 |
| Versão da editora: | https://www.sciencedirect.com/science/article/pii/S2352220822000281 |
| Arbitragem científica: | yes |
| Acesso: | Acesso aberto |
| Aparece nas coleções: |
