Engrácia, P. (2009). Proof-theoretical studies on the bounded functional interpretation.