Refined Complexity Analysis of Cut Elimination. - Philipp Gerhardy (CSL, 2003)

Generalized metatheorems on the extractability of uniform bounds in functional analysis. - Philipp Gerhardy; Ulrich Kohlenbach (Mathematics, Algorithms, Proofs, 2005)

Extracting Herbrand disjunctions by functional interpretation. - Philipp Gerhardy; Ulrich Kohlenbach (Arch. Math. Log., 2005)

The Role of Quantifier Alternations in Cut Elimination. - Philipp Gerhardy (Notre Dame J. Formal Log., 2005)

Strongly uniform bounds from semi-constructive proofs. - Philipp Gerhardy; Ulrich Kohlenbach (Ann. Pure Appl. Log., 2006)

Proof Mining in Topological Dynamics. - Philipp Gerhardy (Notre Dame J. Formal Log., 2008)

Skolem + Tetration Is Well-Ordered. - Mathias Barra; Philipp Gerhardy (CiE, 2009)

The Ordinal of Skolem + Tetration Is tau0. - Mathias Barra; Philipp Gerhardy (CiE, 2010)