Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/32366
Título: | Confluence for classical logic through the distinction between values and computations |
Autor(es): | Espírito Santo, José Matthes, Ralph Nakazawa, Koji Pinto, Luís F. |
Palavras-chave: | Classical logic Confluence Values and computations Monadic meta-language |
Data: | 2014 |
Editora: | Open Publishing Association |
Revista: | Electronic Proceedings in Theoretical Computer Science (EPTCS) |
Resumo(s): | We apply an idea originated in the theory of programming languages - monadic meta-language with a distinction between values and computations - in the design of a calculus of cut-elimination for classical logic. The cut-elimination calculus we obtain comprehends the call-by-name and call-by-value fragments of Curien-Herbelin's lambda-bar-mu-mu-tilde-calculus without losing confluence, and is based on a distinction of "modes" in the proof expressions and "mode" annotations in types. Modes resemble colors and polarities, but are quite different: we give meaning to them in terms of a monadic meta-language where the distinction between values and computations is fully explored. This meta-language is a refinement of the classical monadic language previously introduced by the authors, and is also developed in the paper. |
Tipo: | Artigo em ata de conferência |
Descrição: | Publicado em "Electronic Proceedings in Theoretical Computer Science (EPTCS)", vol. 164 |
URI: | https://hdl.handle.net/1822/32366 |
DOI: | 10.4204/EPTCS.164.5 |
ISSN: | 2075-2180 |
Outros identificadores: | 10.4204/EPTCS.164.5 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
1409.3316v1.pdf | 154,9 kB | Adobe PDF | Ver/Abrir |