Termination of permutative conversions in intuitionistic Gentzen calculi

AbstractIt is shown that permutative conversions terminate for the cut-free intuitionistic Gentzen (i.e. sequent) calculus; this proves a conjecture by Dyckhoff and Pinto. The main technical tool is a term notation for derivations in Gentzen calculi. These terms may be seen as λ-terms with explicit substitution, where the latter corresponds to the left introduction rules