Analyzing Gödel's T Via Expanded Head Reduction Trees
Arnold Beckmann, Andreas Weiermann · Mathematical logic quarterly · 2000
Inspired from Buchholz' ordinal analysis of ID1 and Beckmann's analysis of the simple typed λ-calculus we classify the derivation lengths for Gödel's system T in the λ-formulation (where the η-rule is included).