: Program Extraction from Gentzen's Proof of Transfinite Induction up to epsilon0.
: Modeling Meta-logical Features in a Calculus with Frozen Variables.
: Proof Theory and Post-turing Analysis.
: Interpolation for Natural Deduction with Generalized Eliminations.
: Constructive Foundations for Featherweight Java.