Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/50672
Título: | The polarized λ-calculus |
Autor(es): | Espírito Santo, José |
Palavras-chave: | Polarized logic Focusing Bidirectional natural deduction General elimination rule Eta-expansion |
Data: | 2017 |
Editora: | Elsevier España |
Revista: | Electronic Notes in Theoretical Computer Science |
Resumo(s): | A natural deduction system isomorphic to the focused sequent calculus for polarized intuitionistic logic is proposed. The system comes with a language of proof-terms, named polarized λ-calculus, whose reduction rules express simultaneously a normalization procedure and the isomorphic copy of the cut-elimination procedure pertaining to the focused sequent calculus. Noteworthy features of this natural deduction system are: how the polarity of a connective determines the style of its elimination rule; the existence of a proof-search strategy which is equivalent to focusing in the sequent calculus; the highlydisciplined organization of the syntax - even atoms have introduction, elimination and normalization rules. The polarized λ-calculus is a programming formalism close to call-by-push-value, but justified by its proof-theoretical pedigree. |
Tipo: | Artigo |
URI: | https://hdl.handle.net/1822/50672 |
DOI: | 10.1016/j.entcs.2017.04.010 |
ISSN: | 1571-0661 |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: | CMAT - Artigos em revistas com arbitragem / Papers in peer review journals |