Utilize este identificador para referenciar este registo: https://hdl.handle.net/1822/8427

TítuloCompleting herbelin's programme
Autor(es)Espírito Santo, José
Data2007
EditoraSpringer Verlag
RevistaLecture Notes in Computer Science
CitaçãoINTERNATIONAL CONFERENCE ON TYPED LAMBDA CALCULI AND APPLICATIONS, Paris, 2007 – “International Conference on Typed Lambda Calculi and Applications : (TLCA 2007)”. [S.l.: s. n.,] 2007.
Resumo(s)In 1994 Herbelin started and partially achieved the programme of showing that, for intuitionistic implicational logic, there is a Curry-Howard interpretation of sequent calculus into a variant of the $\lambda$-calculus, specifically a variant which manipulates formally ``applicative contexts'' and inverts the associativity of ``applicative terms''. Herbelin worked with a fragment of sequent calculus with constraints on left introduction. In this paper we complete Herbelin's programme for full sequent calculus, that is, sequent calculus without the mentioned constraints, but where permutative conversions necessarily show up. This requires the introduction of a lambda-like calculus for full sequent calculus and an extension of natural deduction that gives meaning to ``applicative contexts'' and ``applicative terms''. Such extension is a calculus with \emph{modus ponens} and primitive substitution that refines von Plato's natural deduction; it is also a ``coercion calculus'', in the sense of Cervesato and Pfenning. The proof-theoretical outcome is noteworthy: the puzzling relationship between cut and substitution is settled; and cut-elimination in sequent calculus is proven isomorphic to normalisation in the proposed natural deduction system. The isomorphism is the mapping that inverts the associativity of applicative terms.
TipoArtigo em ata de conferência
URIhttps://hdl.handle.net/1822/8427
ISBN9783540732273
ISSN0302-9743
Versão da editorawww.springerlink.com
Arbitragem científicayes
AcessoAcesso aberto
Aparece nas coleções:CMAT - Artigos em atas de conferências e capítulos de livros com arbitragem / Papers in proceedings of conferences and book chapters with peer review

Ficheiros deste registo:
Ficheiro Descrição TamanhoFormato 
HerbelinProgramme(camera-ready).pdf175,55 kBAdobe PDFVer/Abrir

Partilhe no FacebookPartilhe no TwitterPartilhe no DeliciousPartilhe no LinkedInPartilhe no DiggAdicionar ao Google BookmarksPartilhe no MySpacePartilhe no Orkut
Exporte no formato BibTex mendeley Exporte no formato Endnote Adicione ao seu ORCID