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.


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.