Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/39302
Título: | Curry-Howard for sequent calculus at last! |
Autor(es): | Espírito Santo, José |
Palavras-chave: | Co-control Co-continuation Vector notation Let-expression Formal substitution Context substitution Computational lambda-calculus Classical logic de Morgan duality |
Data: | 12-Jun-2015 |
Editora: | Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH |
Revista: | Leibniz International Proceedings in Informatics, LIPIcs |
Resumo(s): | This paper tries to remove what seems to be the remaining stumbling blocks in the way to a full understanding of the Curry-Howard isomorphism for sequent calculus, namely the questions: What do variables in proof terms stand for? What is co-control and a co-continuation? How to define the dual of Parigot's mu-operator so that it is a co-control operator? Answering these questions leads to the interpretation that sequent calculus is a formal vector notation with first-class co-control. But this is just the "internal" interpretation, which has to be developed simultaneously with, and is justified by, an "external" one, offered by natural deduction: the sequent calculus corresponds to a bi-directional, agnostic (w.r.t. the call strategy), computational lambda-calculus. Next, the duality between control and co-control is studied and proved in the context of classical logic, where one discovers that the classical sequent calculus has a distortion towards control, and that sequent calculus is the de Morgan dual of natural deduction. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/39302 |
ISBN: | 9783939897873 |
DOI: | 10.4230/LIPIcs.TLCA.2015.165 |
ISSN: | 1868-8969 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
AtLast.pdf | 555,07 kB | Adobe PDF | Ver/Abrir |
Este trabalho está licenciado sob uma Licença Creative Commons