Permutative conversions in intuitionistic multiary sequent calculus with cuts

• Autor(es): Espírito Santo, José ; Pinto, Luís F.
• Data: 2003
• Identificador Persistente: http://hdl.handle.net/1822/3906
• Origem: RepositóriUM - Universidade do Minho
• Assunto(s): $\lambda$-calculus; Permutative conversions; Sequent calculus
• Tipo de Documento: Documento de conferência
• Idioma: Inglês

Descrição

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.