Part I Reflections.- Gentzen's Consistency Proof in Context, Reinhard Kahle.- Gentzen's Anti-Formalist Views, Michael Detlefsen.- The Use of Trustworthy Principles in a Revised Hilbert's Program, Anton Setzer.- Part II Gentzen's Consistency Proofs.- On Gentzen's First Consistency Proof for Arithmetic, Wilfried Buchholz.- From Hauptsatz to Hilfssatz, Jan von Plato.- A Note on How to Extend Gentzen's Second Consistency Proof to a Proof of Normalization for First Order Arithmetic, Dag Prawitz.- A Direct Gentzen-Style Consistency Proof for Heyting Arithmetic, Annika Siders.- Gentzen's Original Consistency Proof and the Bar Theorem, W.W. Tait.- Goodstein's Theorem Revisited, Michael Rathjen.- Part III Results.- Cut Elimination In Situ, Sam Buss.- Spector's Proof of the Consistency of Analysis, Fernando Ferreira.- Climbing Mount ¿_0, Herman Ruge Jervell.- Semi-Formal Calculi and Their Applications, Wolfram Pohlers.- Part IV Developments.- Proof Theory for Theories of Ordinals III: ¿_N-Reflection, Toshiyasu Arai.- A Proof-Theoretic Analysis of Theories for Stratified Inductive Definitions, Gerhard Jäger and Dieter Probst.- Classifying Phase Transition Thresholds for Goodstein Sequences and Hydra Games, Frederik Meskens and Andreas Weiermann.- Non-deterministic Epsilon Substitution Method for PA and ID_1, Grigori Mints.- A Game-Theoretic Computational Interpretation of Proofs in Classical Analysis, Paulo Oliva and Thomas Powell.- Well-Ordering Principles and Bar Induction, Michael Rathjen and Pedro Francisco Valencia Vizcaíno.