- TU Darmstadt
Friday, March 15, 2019
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 Goedel's functional interpretation in Hilbert's
program and the early days of proof theory. The second and third lectures
comprise a 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.
Prerequisites: A certain knowledge of classical and intuitionistic first-order predicate logic.
8 hours, 1 credit point.
Fri 15 Mar 14:30-16:30 Sala riunioni secondo piano
Mon 18 Mar 09:30-12:30 Sala riunioni secondo piano
Tue 19 Mar 15:30-18:30 Sala riunioni secondo piano
Wed 20 Mar 09:30-12:30 Sala riunioni secondo piano
The three-hours slots of Mon, Tue and Wed are to be understood as follows.
Mon and Tue: two hours lecture with one hour exercises intersparsed.
Wed: one hour overview of proof mining followed by a one-hour research seminar.
Short breaks will be held in between.
This compact course is funded by the John Templeton Foundation within the project "A New Dawn of Intuitionism:
Mathematical and Philosophical Advances'' (ID 60842). The opinions expressed during the course are those of the lecturer
and of the audience, and do not necessarily reflect the views of the John Templeton Foundation.
Web page of Thomas Powell: https://www2.mathematik.tu-darmstadt.de/~powell/