Workshop exploring the intersection of proof theory and computational mathematics through 29 specialized lectures delivered by leading researchers in mathematical logic. Delve into advanced topics including reverse mathematics, fixed point theorems, ordinal analysis, proof mining, and constructive mathematics across five intensive days. Examine cutting-edge research on weak set theories, modal logic proof systems, realizability interpretations, and the computational content of classical mathematical proofs. Investigate the relationship between provability and computation through presentations on natural deduction systems, cyclic proofs, tensorial logic, and dialogue categories. Explore foundational questions in mathematical logic including the Cantor-Bernstein theorem, Gödel's Dialectica interpretation, intuitionistic arithmetic, and ramified type theory. Gain insights into specialized areas such as predicative proof theory, monotone modal logics, expander graphs in bounded arithmetic, and quantitative methods in projection algorithms. Study advanced topics in constructive mathematics including continuity principles, partial proofs in extended predicative universes, and non-deterministic inductive definitions through the lens of reverse mathematics.

Syllabus

Silvia Steila: An overview over least fixed points in weak set theories
Paul Shafer:Reverse mathematics of Caristi's fixed point theorem and Ekeland's variational principle
Iosif Petrakis: Myhill's system CST revisited
Fedor Pakhomov: Reflection ranks and ordinal analysis
Arnold Beckmann: Hyper Natural Deduction
Amir Tabatabai Mining the Surface: Proof mining in the bounded world
Albert Visser: The absorption law for slow provability
Sam Sanders (joint with Dag Normann): Uniformity in mathematics
Anton Freund: Bachmann Howard Fixed Points
Wilfried Sieg: The Cantor Bernstein Theorem How many proofs
Sara Negri: Topological generalizations of possible worlds semantics and their proof systems
Paulo Oliva: On a Dialectica like version of Kleene numerical realizability
Matthias Baaz: Fast cut elimination in intuitionistic logic
Bahareh Afshari: Cyclic Modal Proofs
Lew Gordeew: Predicative proof theory of PDL
Lars Kristiansen: First order concatenation theory vs first order number theory
Gunnar Wilken: Pure Sigma 2 Elementarity beyond the Core
Graham Leigh: On the computational content of classical sequent calculus
Chuangjie Xu: A syntactic approach to continuity and ....
Anton Setzer: The extended predicative Mahlo Universe and the need for partial proofs and .......
Eugenio Orlandelli: Proof theory for quantified monotone modal logics
Sam Buss: Expanders in VNC^1 and Monotone Propositional Proofs
Erik Palmgren: A constructive examination of a Russell style ramified type theory
Harry Altman: Lower sets in products of well ordered sets
Andrei Sipos: Quantitative results on the method of averaged projections
Paul Andre Mellies: An introduction to tensorial logic and dialogue categories
Benno van den Berg: Two observations on intuitionistic logic and arithmetic
Giuseppe Rosolini: Triposes and Gödel's Dialectica Interpretation
Hajime Ishihara: Reverse mathematics of non deterministic inductive definitions
Hugo Herbelin: Computing with Markov's principle