Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/73099| Título: | The call-by-value Lambda-Calculus with generalized applications |
| Autor(es): | Espírito Santo, José |
| Palavras-chave: | Generalized applications Natural deduction Standardization Call-by-value Protecting-by-a-lambda Call-by-name Strong normalization |
| Data: | 2020 |
| Editora: | Schloss Dagstuhl - Leibniz-Zentrum für Informatik |
| Revista: | Leibniz International Proceedings in Informatics, LIPIcs |
| Resumo(s): | The lambda-calculus with generalized applications is the Curry-Howard counterpart to the system of natural deduction with generalized elimination rules for intuitionistic implicational logic. In this paper we identify a call-by-value variant of the system and prove confluence, strong normalization, and standardization. In the end, we show that the cbn and cbv variants of the system simulate each other via mappings based on extensions of the "protecting-by-a-lambda" compilation technique. |
| Tipo: | Artigo em ata de conferência |
| URI: | https://hdl.handle.net/1822/73099 |
| ISBN: | 978-3-95977-132-0 |
| DOI: | 10.4230/LIPIcs.CSL.2020.35 |
| ISSN: | 1868-8969 |
| Versão da editora: | https://drops.dagstuhl.de/opus/volltexte/2020/11678/ |
| Arbitragem científica: | yes |
| Acesso: | Acesso aberto |
| Aparece nas coleções: |
Este trabalho está licenciado sob uma Licença Creative Commons
