Cut-elimination and a permutation-free sequent calculus for intuitionistic logic
scientific article; zbMATH DE number 1501369