Permutative conversions in intuitionistic multiary sequent calculi with cuts

Abstract

This work presents an extension with cuts of Schwichtenberg's multiary sequent calculus. We identify a set of permutative conversions on it, prove their termination and confluence and establish the permutability theorem. We present our sequent calculus as the typing system of the {\em generalised multiary $\lambda$-calculus} lambda-Jm, a new calculus introduced in this work. Lambda-Jm corresponds to an extension of $\lambda$-calculus with a notion of {\em generalised multiary application}, which may be seen as a function applied to a list of arguments and then explicitly substituted in another term. Proof-theoretically the corresponding typing rule encompasses, in a modular way, generalised eliminations of von Plato and Herbelin's head cuts.