Computation-Sensitive Proofs

Proof mining stands for the process of logically analysing formal proofs with the aim of obtaining new (hidden) information from such proofs. For instance, a proof that certain iteration of a function converges to one of its fixed point might have hidden information about the rate at which the sequence converges (rate of convergence), or, a proof that a continuous function has a unique best approximation will normally contain a (potentially implicit) algorithm for constructing the polynomial out of any given function (modulus of uniqueness). The extraction of computational information from ineffective proofs often require a systematic analysis guided by methods of proof theory, such as proof translations and functional interpretations (e.g. realizability). These techniques have recently been shown to yield new interesting mathematical theorems out of old proofs, particularly in functional analysis (approximation theory and fixed point theory). The proposed project aims to develop new proof mining techniques and carry out concrete case studies in both computer science and mathematics, with the emphasis on the role of the structural rule of contraction in the complexity of the extracted programs. We will focus on the recent technique of hybrid functional interpretation which allows optimal use of several functionals interpretations when analysing a single proof. The technique will be implemented in a proof assistant, and case studies will be carried out.