Completing Herbelin's Programme

Abstract. 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 λ-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

• Type: Conference
• Year: 2007
• Where: TLCA
• Authors: José Espírito Santo
• Keywords: Applicative Contexts, Intuitionistic Implicational Logic, Sequent Calculus, Theoretical Computer Science, TLCA 2007