Applied Proof Theory and the Computational Content of Mathematics

M1. Applied Proof Theory and the Computational Content of Mathematics

Organisers: Thomas Powell (TU Darmstadt) and Sam Sanders (LMU Munich)

Proof theory is one of the pillars of mathematical logic, and is centered around the idea of treating proofs as mathematical objects which can be formally analysed. While proof theory has its origin in the early 20th century, where it was primarily concerned with foundational problems, modern proof theory is far more focused on applications. In the last few decades the use of sophisticated proof theoretic techniques to extract computational content from proofs has led to important new quantitative results in both mathematics and computer science.

The aim of this symposium is to provide an overview of some exciting recent developments in applied proof theory, and to showcase several new areas in which proof theory is playing a role. The symposium will take place on Thursday 14 September, and will consist of ten talks:

10.15-10.45	Ulrich Kohlenbach (TU Darmstadt)
	Proof Mining in Convex Optimization
10.45-11.15	Fernando Ferreira (University of Lisbon)
	A herbrandized functional interpretation of first and second-order arithmetic
11.15-11.45	Helmut Schwichtenberg (LMU Munich)
	E-arithmetic
11.45-12.15	Peter Schuster (University of Verona)
	Extension by conservation: from transfinite to finite proof methods in abstract algebra
12.15-12.45	Thomas Powell (TU Darmstadt)
	Proof interpretations with imperative features
12.45-15.30	LUNCH BREAK
15.30-16.00	Sam Sanders (LMU Munich)
	Metastability, computability theory, and Nonstandard Analysis
16.00-16.30	Chuangjie Xu (LMU Munich)
	Extracting Computer Programs from Nonstandard Proofs
16.30-17.00	Silvia Steila (University of Bern)
	On some fixed point statements over Kripke Platek
17.00-17.30	Federico Aschieri (TU Vienna)
	Games Semantics and the Complexity of Cut-Elimination
17.30-18.00	Kenji Miyamoto (University of Innsbruck)
	Complexity Analysis for Epsilon-Calculus

This minisymposium is supported by the Deutsche Vereinigung für Mathematische Logik und für Grundlagenforschung der Exakten Wissenschaften (DVMLG).