Utilize este identificador para referenciar este registo:
https://hdl.handle.net/1822/8427
Título: | Completing herbelin's programme |
Autor(es): | Espírito Santo, José |
Data: | 2007 |
Editora: | Springer Verlag |
Revista: | Lecture Notes in Computer Science |
Citação: | INTERNATIONAL 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. |
Tipo: | Artigo em ata de conferência |
URI: | https://hdl.handle.net/1822/8427 |
ISBN: | 9783540732273 |
ISSN: | 0302-9743 |
Versão da editora: | www.springerlink.com |
Arbitragem científica: | yes |
Acesso: | Acesso aberto |
Aparece nas coleções: |
Ficheiros deste registo:
Ficheiro | Descrição | Tamanho | Formato | |
---|---|---|---|---|
HerbelinProgramme(camera-ready).pdf | 175,55 kB | Adobe PDF | Ver/Abrir |