
Logic & Semantics 
With the term `proof mining' we denote the activity of transforming a prima facie nonconstructive proof into a new one from which certain computational information can be read off which was not visible beforehand.
Already in the 50's Georg Kreisel realized that logical techniques from proof theory  originally developed for foundational purposes  can be put to use here. In recent years, a more systematic proof theoretic approach to proof mining in numerical analysis emerged yielding new quantitative (and even qualitative) numerical results in approximation theory and fixed point theory and providing a bridge between mathematical numerical analysis and the area of computability (and complexity) in analysis which has mainly been developed by logicians (and complexity theorists).
Although proof mining has been applied also to e.g. number theory and combinatorics, the area of numerical (functional) analysis is of particular interest since here noneffectivity is at the core of many principles (like compactness arguments) which are used to ensure convergence. In mathematical terms this noncomputability often is an obstacle to obtain a quantitative stability analysis and rates of convergence.
We will give a survey and discuss two recent applications concerning
(i) new uniform bounds for theorems of Ishikawa and BorweinReichShafrir on the asymptotic regularity of nonexpansive mappings yielding even new qualitative results,
(ii) fully explicit description of the rate of strong unicity for best L_1approximations of continuous functions by polynomials (joint work with Paulo Oliva).