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).
We acknowledge the support of
