Room P3.10, Mathematics Building

José Espírito Santo, U Minho

A lambda-calculus for sequent calculus

We present the "generalised multiary lambda-calculus" (gm-lambda), an extension of the lambda-calculus that corresponds, in the Curry-Howard sense, to a fragment of sequent calculus. Our system is obtained as a generalisation of a system of Schwichtenberg, by allowing a class of cuts and rules for cut- elimination. It also captures, as subsystems, other calculi already known in the literature. Indeed, one of the constructors of gm-lambda is a general kind of application, whose typing rule is an amalgamation of von Plato's generalised elimination rule and Herbelin's head-cut. The computational reading of such construction is as a function applied to a list of arguments and then explicitly substituted in another term. We define a set of permutative conversions, prove its confluence and termination and establish the permutability theorem: two gm-terms determine the same lambda-term iff they are inter-permutable. (This is joint work with Luis Pinto, UM.)