Permutative conversions in intuitionistic multiary sequent calculus with cuts

• Author(s): Espírito Santo, José ; Pinto, Luís F.
• Date: 2003
• Persistent ID: http://hdl.handle.net/1822/3906
• Origin: RepositóriUM - Universidade do Minho
• Subject(s): $\lambda$-calculus; Permutative conversions; Sequent calculus
• Document Type: Conference Object
• Language: English

Description

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.