Completing Herbelin's Programme

10 years 1 months ago
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
José Espírito Santo
Added 09 Jun 2010
Updated 09 Jun 2010
Type Conference
Year 2007
Where TLCA
Authors José Espírito Santo
Comments (0)