Schedule of the Summer School
Thursday, May 3
| 10:00 - 10:30 | Registration and welcome coffee |
| 10:30 - 11:30 | Michael Rathjen: Opening and Introduction |
| 11:30 - 12:30 | Peter Dybjer: Intuitionistic Type Theory (Lecture I) |
| 12:30 - 15:00 | Lunch break |
| 15:00 - 16:00 | Ulrich Kohlenbach: Extraction of Information from Proofs (Lecture I) |
| 16:00 - 16:30 | Tea and cake |
| 16:30 - 17:30 | Andreas Weiermann: Higher Proof Theory and Combinatorics (Lecture I) |
| 17:30 - 18:30 | Matthew Hendtlass: Constructive Analysis (Lecture I) |
| 18:30 - | Reception |
Friday, May 4
| 09:00 - 10:00 | Thierry Coquand: Constructive Algebra (Lecture I) |
| 10:00 - 10:30 | Group photo and coffee break |
| 10:30 - 11:30 | Ulrich Kohlenbach: Extraction of Information from Proofs (Lecture II) |
| 11:30 - 12:30 | Andreas Weiermann: Higher Proof Theory and Combinatorics (Lecture II) |
| 12:30 - 15:00 | Lunch break |
| 15:00 - 16:00 | Peter Aczel: Constructive Set Theory (Lecture I) |
| 16:00 - 16:30 | Tea and cake |
| 16:30 - 17:30 | Peter Dybjer: Intuitionistic Type Theory (Lecture II) |
| 17:30 - 18:30 | Simon Huber: Homotopy Type Theory (Lecture I) |
Saturday, May 5
| 08:30 - 09:30 | Ulrich Kohlenbach: Extraction of Information from Proofs (Lecture III) |
| 09:30 - 10:30 | Andreas Weiermann: Higher Proof Theory and Combinatorics (Lecture III) |
| 10:30 - 11:00 | Coffee break |
| 11:00 - 12:00 | Peter Aczel: Constructive Set Theory (Lecture II) |
| 12:00 - 13:00 | Simon Huber: Homotopy Type Theory (Lecture II) |
Sunday, May 6
| No program - access to the institute only for registered long-term visitors with access card |
Monday, May 7
| 09:00 - 10:00 | Martin Hötzel Escardó: Constructive Mathematics in Univalent Type Theory (Lecture I) |
| 10:00 - 10:30 | Coffee break |
| 10:30 - 11:30 | Matthews Hendtlass: Constructive Analysis (Lecture II) |
| 11:30 - 12:30 | Isabel Oitavem: Recursion and Complexity (Lecture I) |
| 12:30 - 15:00 | Lunch break |
| 15:00 - 16:00 | Peter Dybjer: Intuitionistic Type Theory (Lecture III) |
| 16:00 - 16:30 | Tea and cake |
| 16:30 - 17:30 | Simon Huber: Homotopy Type Theory (Lecture III) |
| 17:30 - 18:30 | Robert Constable: Proof Assistants and Formalization (Lecture I) |
| 19:30 - | Dinner - Brauhaus Bönnsch, Sterntorbrücke 4, Bonn, www.boennsch.de, Dutch treat |
Tuesday, May 8
| 9:00 - 10:00 | Martin Hötzel Escardó: Constructive Mathematics in Univalent Type Theory (Lecture II) |
| 10:00 - 10:30 | Coffee break |
| 10:30 - 11:30 | Thierry Coquand: Constructive Algebra (Lecture II) |
| 11:30 - 12:30 | Matthew Hendtlass: Constructive Analysis (Lecture III) |
| 12:30 - 15:00 | Lunch break |
| 15:00 - 16:00 | Isabel Oitavem: Recursion and Complexity (Lecture II) |
| 16:00 - 16:30 | Tea and cake |
| 16:30 - 17:30 | Robert Constable: Proof Assistants and Formalization (Lecture II) |
| 17:30 - | Problems and questions |
Wednesday, May 9
| 9:00 - 10:00 | Peter Aczel: Constructive Set Theory (Lecture III) |
| 10:00 - 10:30 | Coffee break |
| 10:30 - 11:30 | Thierry Coquand: Constructive Algebra (Lecture III) |
| 11:30 - 12:30 | Isabel Oitavem: Recursion and Complexity (Lecture III) |
| 12:30 - 15:00 | Lunch break |
| 15:00 - 16:00 | Robert Constable: Proof Assistants and Formalization (Lecture III) |
| 16:00 - 16:30 | Tea and cake |
| 16:30 - 17:30 | Martin Hötzel Escardó: Constructive Mathematics in Univalent Type Theory (Lecture III) |
| 17:30 - | Problems and questions |
Abstracts and teaching materials
Michael Rathjen: Opening and Introduction
Robert Constable: Proof Assistants and Formalization
Teaching materials to Mark Bickford's Skype talk on Wednesday
Thierry Coquand: Constructive Algebra
Recorded Talks:
Lecture I
Lecture II
Lecture III
Peter Dybjer: Intuitionistic Type Theory
Recorded talks:
Lecture I
Lecture II
Lecture III
Ulrich Kohlenbach: Extraction of Information from Proofs
Recorded Talks:
Isabel Oitavem: Recursion and Complexity
Computability theory provides us with theoretical results about what can be computed. However, just a fraction of the theoretically computable functions can be implemented through efficient algorithms. Complexity theory addresses this question, usually using machine models, like the Turing machine, and explicit bounds. In contrast, implicit characterizations of complexity classes avoid both machines and explicit complexity conditions and therefore allow a more mathematically description of complexity classes. In this minicourse different characterisations of complexity classes based on recursive schemes will be discussed.
Andreas Weiermann: Higher Proof Theory and Combinatorics
Recorded Talks:
Martin Hötzel Escardó: Constructive Mathematics in Univalent Type Theory
Recorded Talks: