Eyvind Briseid

Title: Proof mining and effective metric fixed point theory.

Abstract: Using logical metatheorems for functional analysis developed by 
Kohlenbach and Gerhardy one can in many cases under rather general 
conditions systematically find computable and to a high degree uniform 
rates of convergence for the Picard iteration sequences for nonexpansive 
selfmaps of metric spaces. For concrete and important cases we have been 
able to find such explicit rates of convergence even when the mappings 
were not necessarily nonexpansive. We here give an explanation in logical 
terms for most of these results by invoking a novel use of the logical 
metatheorems in question.