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" |
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" |
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" |
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" |
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" |