Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/39302
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | por |
dc.date.accessioned | 2016-01-08T14:02:24Z | - |
dc.date.available | 2016-01-08T14:02:24Z | - |
dc.date.issued | 2015-06-12 | - |
dc.identifier.isbn | 9783939897873 | por |
dc.identifier.issn | 1868-8969 | por |
dc.identifier.uri | https://hdl.handle.net/1822/39302 | - |
dc.description.abstract | 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. | por |
dc.description.sponsorship | (undefined) | por |
dc.language.iso | eng | por |
dc.publisher | Schloss Dagstuhl – Leibniz-Zentrum für Informatik GmbH | por |
dc.relation | info:eu-repo/grantAgreement/FCT/5876/135888/PT | por |
dc.rights | openAccess | por |
dc.rights.uri | http://creativecommons.org/licenses/by/4.0/ | por |
dc.subject | Co-control | por |
dc.subject | Co-continuation | por |
dc.subject | Vector notation | por |
dc.subject | Let-expression | por |
dc.subject | Formal substitution | por |
dc.subject | Context substitution | por |
dc.subject | Computational lambda-calculus | por |
dc.subject | Classical logic | por |
dc.subject | de Morgan duality | por |
dc.title | Curry-Howard for sequent calculus at last! | por |
dc.type | conferencePaper | - |
dc.peerreviewed | yes | por |
sdum.publicationstatus | published | por |
oaire.citationConferenceDate | 01 - 03 Jul. 2015 | por |
sdum.event.type | conference | por |
oaire.citationStartPage | 165 | por |
oaire.citationEndPage | 179 | por |
oaire.citationConferencePlace | Warsaw, Poland | por |
oaire.citationTitle | 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) | por |
oaire.citationVolume | 38 | por |
dc.identifier.doi | 10.4230/LIPIcs.TLCA.2015.165 | por |
dc.subject.fos | Ciências Naturais::Matemáticas | por |
sdum.journal | Leibniz International Proceedings in Informatics, LIPIcs | por |
sdum.conferencePublication | 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015) | por |
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