## Program (click for a .pdf) and Slides of some Talks

### Monday, September 9

14:00** Opening Address by Prof. Dr. Martin Täuber, Rector of the University of Bern**

Chair: Godehard Link

14:15 | – | 15:00 | Volker Halbach "Provability, Self-Reference and Intensionality" |

15:00 | – | 15:45 | Jan von Plato "Saved from the Cellar: Gentzen's Shorthand Notes |

on Logic and Foundations" |
|||

15:45 | – | 16:15 | Coffee break |

16:15 | – | 17:00 | Stefania Centrone "Rigorous Proofs and the Ban on |

the 'metábasis eis állo génos' in B. Bolzano" |
|||

17:00 | – | 17:30 | Coffee break |

17:30 | – | 18:00 | Bahare Afshari & Graham Leigh "Closure Ordinals for the Modal μ-Calculus" |

18:00 | – | 18:30 | Takako Nemoto "Ramified Analysis Revisited: |

A Refinement of Determinacy Hierarchy" |

### Tuesday, September 10

Chair: Andrea Cantini

09:15 | – | 10:00 | Roman Murawski "On Proof in Mathematics – Philosophical Remarks" |

10:00 | – | 10:30 | Coffee break |

10:30 | – | 11:15 | Kosta Dosen "Proof Theory and Deduction Theory" |

11:15 | – | 12:00 | Gerhard Jäger "Operational Set Theory with Classes" |

*Lunch break*

Chair: Wolfram Pohlers

14:00 | – | 14:45 | Michael Rathjen "Calibrating the Proof Power of Type Theories" |

14:45 | – | 15:30 | Thomas Strahm "Unfolding Schematic Systems: a Survey" |

15:30 | – | 16:00 | Coffee break |

16:00 | – | 16:45 | Stan Wainer "A Hierarchy of Ramified Theories Extending PRA" |

16:45 | – | 17:30 | Giuseppe Rosolini "Intrinsic Sobriety" |

17:30 | – | 18:00 | Coffee break |

18:00 | – | 18:45 | Dana Scott "A Stochastic Lambda-Calculus" |

### Wednesday, September 11

Chair: Wilfried Buchholz

09:15 | – | 10:00 | Laura Crosilla "Philosophical Reflections On Constructive Mathematics" |

10:00 | – | 10:30 | Coffee break |

10:30 | – | 11:15 | Hajime Ishihara "Classical Propositional Logic and |

Decidability of Variables in Intuitionistic Propositional Logic" |
|||

11:15 | – | 12:00 | Giovanni Sambin "Benefits of a Minimalist Foundation" |

*Lunch break*

Chair: Peter Aczel

14:00 | – | 14:45 | Ulrich Berger "How Constructive is Abstract Mathematics?" |

14:45 | – | 15:30 | Josef Berger "Higman's Lemma and Dickson's Lemma are equivalent" |

15:30 | – | 16:00 | Coffee break |

16:00 | – | 16:45 | Steve Awodey "Advances in Univalent Foundations" |

16:45 | – | 17:30 | Thierry Coquand "On the Computational Content of the Axiom of Univalence" |

17:30 | – | 18:00 | Coffee break |

18:00 | – | 18:45 | Erik Palmgren "Remarks on Dependently Typed First Order Logic" |

### Thursday, September 12

Chair: Pavel Pudlak

09:15 | – | 10:00 | Helmut Schwichtenberg "Proofs and Computations" |

10:00 | – | 10:30 | Coffee break |

10:30 | – | 11:15 | Vivek Nigam "An Extended Framework for Specifying |

and Reasoning about Proof Systems" |
|||

11:15 | – | 12:00 | Ulrich Kohlenbach "On the Finitary Content of non-effective Proofs |

in non-linear Analysis" |

*Lunch break*

Chair: Marco Benini

14:00 | – | 14:45 | Georges Gonthier "A Computer-Checked Proof of the Odd Order Theorem" |

14:45 | – | 15:30 | Russell O'Connor "My 10 years of Computer Verified Mathematics or: |

How I Learned to Stop Worrying and Love Constructive Mathematics" |
|||

15:30 | – | 16:00 | Coffee break |

16:00 | – | 16:45 | Matthias Baaz "Towards a Proof Theory of Analogical Reasoning" |

16:45 | – | 17:30 | Peter Koepke "Formal Modeling of Reasoning in Natural Language Proofs" |

17:30 | – | 18:00 | Coffee break |

18:00 | – | 18:30 | Enno Aufderheide "Funding Opportunities throughout |

the Academic Career – the Humboldt-Foundation Programs" |

*Social dinner*at the Restaurant Dählhölzli.

### Friday, September 13

Chair: Pierluigi Minari

09:15 | – | 10:00 | Assia Mahboubi "Automated and (Formally) Certified Proofs |

of Summation Formulae" |
|||

10:00 | – | 10:30 | Coffee break |

10:30 | – | 11:15 | Ioana Leustean "Linearity Issues in Lukasiewicz logic" |

11:15 | – | 12:00 | Etienne Lozes "Separation logic, its Magic Wand, and some Magic Tricks" |