By Pedro Pinto (Technische Universitat Darmstadt).
Abstract: The classical bounded functional interpretation  was recently shown to be a valid technique to employ in the proof mining practice . In this talk, I will discuss some subtle features of recent "minings" guided by this functional interpretation. I will talk about the quantitative version of the metric projection argument. Next, we will look at the quantitative treatment of a nontrivial discussion by cases and how it guided the recent analysis in . We finish with some brief considerations about metastability results.
 F. Ferreira, Injecting uniformities into Peano Arithmetic, Annals of Pure and Applied Logic, 157 (2009), pp. 122–129.
 F. Ferreira, L. Leustean, and P. Pinto, On the removal of weak compactness arguments in proof mining, Advances in Mathematics, 354 (2019).
 P. Pinto, Proof mining with the bounded functional interpretation, PhD thesis, Universidade de Lisboa, 2019.
 B. Dinis and P. Pinto, Quantitative results on the multi-parameters proximal point algorithm, arXiv preprint 1912.10175, (2019).