Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/32366
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | por |
dc.contributor.author | Matthes, Ralph | por |
dc.contributor.author | Nakazawa, Koji | por |
dc.contributor.author | Pinto, Luís F. | por |
dc.date.accessioned | 2015-01-06T10:42:20Z | - |
dc.date.available | 2015-01-06T10:42:20Z | - |
dc.date.issued | 2014 | - |
dc.identifier | 10.4204/EPTCS.164.5 | - |
dc.identifier.issn | 2075-2180 | por |
dc.identifier.uri | https://hdl.handle.net/1822/32366 | - |
dc.description | Publicado em "Electronic Proceedings in Theoretical Computer Science (EPTCS)", vol. 164 | por |
dc.description.abstract | 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. | por |
dc.description.sponsorship | Fundação para a Ciência e a Tecnologia (FCT) | por |
dc.language.iso | eng | por |
dc.publisher | Open Publishing Association | por |
dc.rights | openAccess | por |
dc.subject | Classical logic | por |
dc.subject | Confluence | por |
dc.subject | Values and computations | por |
dc.subject | Monadic meta-language | por |
dc.title | Confluence for classical logic through the distinction between values and computations | por |
dc.type | conferencePaper | - |
dc.peerreviewed | yes | por |
sdum.publicationstatus | published | por |
oaire.citationConferenceDate | 13 Jul. 2014 | por |
sdum.event.type | conference | por |
oaire.citationStartPage | 63 | por |
oaire.citationEndPage | 77 | por |
oaire.citationIssue | 164 | por |
oaire.citationConferencePlace | Vienna, Austria | por |
oaire.citationTitle | Fifth International Workshop on Classical Logic and Computation (CL&C'14) | por |
oaire.citationVolume | 164 | por |
dc.identifier.doi | 10.4204/EPTCS.164.5 | por |
dc.subject.fos | Ciências Naturais::Matemáticas | por |
dc.subject.fos | Ciências Naturais::Ciências da Computação e da Informação | por |
dc.subject.wos | Science & Technology | por |
sdum.journal | Electronic Proceedings in Theoretical Computer Science (EPTCS) | por |
sdum.conferencePublication | Fifth International Workshop on Classical Logic and Computation (CL&C'14) | por |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
1409.3316v1.pdf | 154,9 kB | Adobe PDF | Ver/Abrir |