Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/11161
Registo completo
Campo DC | Valor | Idioma |
---|---|---|
dc.contributor.author | Espírito Santo, José | - |
dc.date.accessioned | 2010-11-30T17:40:29Z | - |
dc.date.available | 2010-11-30T17:40:29Z | - |
dc.date.issued | 2010 | - |
dc.identifier.citation | DAWAR, Anuj ; VEITH , Helmut, ed. lit. – “Computer science logic : proceedings of the Annual Conference of the EACSL, 19, Brno, Czech Republic, 2010”. Berlin : Springer, cop. 2010. ISBN 978-3-642-15204-7. p. 290-304. | por |
dc.identifier.isbn | 9783642152047 | por |
dc.identifier.issn | 0302-9743 | por |
dc.identifier.uri | https://hdl.handle.net/1822/11161 | - |
dc.description.abstract | This paper studies a new classical natural deduction system, presented as a typed calculus named $\lml$. It is designed to be isomorphic to Curien-Herbelin's calculus, both at the level of proofs and reduction, and the isomorphism is based on the correct correspondence between cut (resp. left-introduction) in sequent calculus, and substitution (resp. elimination) in natural deduction. It is a combination of Parigot's $\lambda\mu$-calculus with the idea of ``coercion calculus'' due to Cervesato-Pfenning, accommodating let-expressions in a surprising way: they expand Parigot's syntactic class of named terms. This calculus aims to be the simultaneous answer to three problems. The first problem is the lack of a canonical natural deduction system for classical logic. $\lml$ is not yet another classical calculus, but rather a canonical reflection in natural deduction of the impeccable treatment of classical logic by sequent calculus. The second problem is the lack of a formalization of the usual semantics of Curien-Herbelin's calculus, that explains co-terms and cuts as, respectively, contexts and hole-filling instructions. The mentioned isomorphism is the required formalization, based on the precise notions of context and hole-expression offered by $\lml$. The third problem is the lack of a robust process of ``read-back'' into natural deduction syntax of calculi in the sequent calculus format, that affects mainly the recent proof-theoretic efforts of derivation of $\lambda$-calculi for call-by-value. An isomorphic counterpart to the $Q$-subsystem of Curien-Herbelin's-calculus is derived, obtaining a new $\lambda$-calculus for call-by-value, combining control and let-expressions. | por |
dc.description.sponsorship | Fundação para a Ciência e a Tecnologia (FCT) | por |
dc.language.iso | eng | por |
dc.publisher | Springer | por |
dc.rights | openAccess | por |
dc.title | Towards a canonical classical natural deduction system | por |
dc.type | conferencePaper | por |
dc.peerreviewed | yes | por |
dc.relation.publisherversion | www.springerlink.com | por |
sdum.pagination | 290-304 | por |
sdum.publicationstatus | published | por |
oaire.citationConferenceDate | 23 Ago. - 27 Ago. 2010 | por |
sdum.event.location | Brno, República Checa | por |
sdum.event.title | 19th EACSL Annual Conference on Computer Science Logic | por |
sdum.event.type | conference | por |
oaire.citationStartPage | 290 | por |
oaire.citationEndPage | 304 | por |
oaire.citationVolume | 6247 | por |
dc.identifier.doi | 10.1007/978-3-642-15205-4_24 | por |
dc.subject.wos | Science & Technology | por |
sdum.journal | Lecture Notes in Computer Science | por |
sdum.conferencePublication | COMPUTER SCIENCE LOGIC | por |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
TowardsClassicalNatDed.pdf | 232,13 kB | Adobe PDF | Ver/Abrir |