UNSERE CHRONIK

Montag, 30. Mai 2022

Proof and Computation 2022

International meeting from 30 May to 2 June 2022 at Cohaus Schlehdorf in Bavaria
Proofs in mathematical practice serve to warrant the truth of mathematical theorems. Proof theory arose with Hilbert's programme to put abstract mathematics on a firm basis by proving consistency in the meta-mathematics and by finite methods only. Gödel's incompleteness theorems have allegedly dashed Hilbert's programme as such but thus have stood at the beginning of a seminal paradigm shift in proof theory: to see mathematical proofs also as a rich source of computational information such as certified algorithms and effective bounds. Contemporary research in this fertile area is known under terms such as dynamical methods, program extraction and proof mining.

Incidentally, today's quest for safety and reliability of data and algorithms is very similar to the debate on foundations of mathematics about a century ago which culminated in Hilbert's and Gödel's advances---today, however, with grave consequences for technology and economy. The key to solving these problems of the digital society up to artificial intelligence is to be found in the logical grounding of mathematics and computer science themselves, the current development of which leads to new joint research methods and perspectives in mathematics and computer science.

In this vein, an international meeting will be held from 30 May to 2 June 2022 at Cohaus Schlehdorf in Bavaria. The aim of this meeting is to bring together eminent scholars and young researchers active in the foundations of mathematics and computer science. There will be ample opportunity to form ad-hoc groups working on specific projects, but also to discuss in more general terms the vision of extracting computational information from proofs. The participants' expertise will include ordinal analysis, predicative foundations, constructive mathematics, type theory, computation in higher types, proof mining and program extraction from proofs

Programme

Monday, 30 May

9:15 - 10:00
Welcome / Klaus Mainzer (TUM, EASA): Proof and Computation. Perspectives for Mathematics, Computer Science, and Philosophy

10:00 - 10:30
Arndt Bode (BAdW)
Benedikt Löwe (DVMLG)
Hajime Ishihara (JAIST)
Franz Merkl (LMU)

10:30 - 11:00
Coffee break

11:00 - 11:45
Stan Wainer (University of Leeds): Functions and Ordinals

11:45 - 12:30
Anton Freund (TU Darmstadt): On a uniform Kruskal-Friedman theorem

Lunch break

14:30 - 14:45
Martin Wirsing (LMU)

14:45 - 15:30
Gerhard Jäger (University of Bern): Gentzen in the 3- and 4-Valued Jungle

15:30 - 16:00
Coffee break

16:00 - 16:45
Dag Normann (University of Oslo): A recent development in the computability theory for functionals of type 3

16:45 - 17:30
Hideki Tsuiki (Kyoto University): Induction / coinduction and projections of fractals

19:00
Dinner at Hotel Klosterbräu

Tuesday, 31 May

9:00 - 9:45
Michael Rathjen (University of Leeds): Paralipomena zur Beweistheorie

9:45 - 10:30
Ulrich Kohlenbach (TU Darmstadt): The Computational Content of Proofs: Applications in Optimization and Ergodic Theory

10:30 - 11:00
Coffee break

11:00 - 11:45
Isabel Oitavem (NOVA University Lisbon): Relativized Classes in Implicit Complexity

11:45 - 12:30
Matthias Baaz (TU Wien): Cut-elimination for prenex cuts in intuitionistic logic without v is elementary

Lunch break

14:00 - 14:45
Laura Crosilla (University of Oslo): On Weyl's predicative concept of set

14:45 - 15:30
Fredrik Forsberg (University of Strathclyde): Constructive Ordinal Theory in Homotopy Type Theory

15:30 - 16:00
Coffee break

Social programme (optional)

16:30
Boat trip (alternatively hike) to Seehotel Grauer Bär

19:00
Dinner at Seehotel Grauer Bär

Wednesday, 1 June

9:00 - 9:45
Henk Barendregt (Radboud University): A lambda calculus satellite

9:45 - 10:30
Anton Setzer (Swansea University): Formalising Martin-Löf's Meaning Explanations for Type Theory in Agda

10:30 - 11:00
Coffee break

11:00 - 11:45
Hans Leiß (LMU Munich): Fixed-point closure of *-continuous Kleene algebras

11:45 - 12:30
Matthias Eberl (ind.): Don't forget the universal quantifier

Lunch break

Working groups

15:30 - 16:00
Coffee break

Working groups

Thursday, 2 June

9:00 - 9:45
Thorsten Altenkirch (University of Nottingham): Normalisation by Evaluation

9:45 - 10:30
Ingo Blechschmidt (University of Padua): Reifying dynamical algebra: maximal ideals for arbitrary rings, constructively

10:30 - 11:00
Coffee break

11:00 - 11:30
Holger Thies (Kyoto University): From Coq Proofs to Efficient Certified Exact Real Computation

11:30 - 12:00
Nils Köpp (LMU Munich): Tree representation of continuous functions on (pre-)Gray-code

12:00 - 12:30
Franziskus Wiesnet (TU Wien): Par means Parallel: Multiplicative Linear Logic as Concurrent Functional Programs

Lunch break

14:00 - 14:30
Olga Petrovska (Swansea University): Operational Semantics for Prawf

14:30 - 15:00
Reinhard Kahle (University of Tübingen): surprise

15:00: - 15:30
Helmut Schwichtenberg (LMU Muenchen): tba