M.-D. Hernest and U. Kohlenbach, “A Complexity Analysis of Functional Interpretations”, BRICS, vol. 10, no. 12, Feb. 2003.