Title: Proof Notations and Cut-Elimination

Abstract:

Using appropriate notation systems for proofs, continuous cut-reduction can
often be rendered feasible on these notations. Explicit bounds
can be given. Applying these bounds to a suitable notation system for
Bounded Arithmetic, all the known results on definable functions of
certain such theories can be reobtained in a uniform way.