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

Robert Constable: Proof Assistants and Formalization

Teaching materials to Mark Bickford's Skype talk on Wednesday

Top

Thierry Coquand: Constructive Algebra

Teaching materials

Top

Peter Dybjer: Intuitionistic Type Theory

Teaching materials

Top

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. 

Top