Compact Course & Research Seminar

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.