**Proof interpretations: A modern perspective**

Thomas Powell (Technische Universität Darmstadt)

The aim of this course is to provide an introduction to proof

interpretations and program extraction, up to the point where some of

their applications in modern mathematics and computer science can be

understood. I begin in the first lecture with a broad historical overview,

tracing the origins of Gödel’s functional interpretation in Hilbert’s

program and the early days of proof theory. The second and third lectures

comprise an introduction to the extraction of computational content from

proofs, both in the intuitionistic and classical setting. I conclude with

a high level overview of the proof mining program, and present some recent

applications of program extraction in functional analysis.

Fri 15 Mar 14:30-16:30

Mon 18 Mar 09:30-12:30

Tue 19 Mar 15:30-18:30

Wed 20 Mar 09:30-12:30

___

The lecture on Wednesday will comprise a research seminar:

**A new application of proof mining in the fixed point theory of uniformly convex Banach spaces**

Proof mining is a branch of proof theory which makes use of

proof theoretic techniques to extract quantitative information from

seemingly nonconstructive proofs. In this talk, I present a new

application of proof mining in functional analysis, which focuses on the

convergence of Picard iterates for generalisations of nonexpansive

mappings in uniformly convex Banach spaces.

___

Venue:

Dipartimento di Informatica, Università di Verona

37134 Verona, Strada Le Grazie 15,

Cà Vignal 2, 2nd floor, sala riunioni

For further information, please see the course webpage.