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