A sequence of lecture about proof theory and Buchholz' Omega rule (Braga, 2004)
A presentation of Novikov's cut-elimination. The interest is that it applies also to non well-founded formulae