The first two and a half days will be reserved for more introductory talks and tutorials, mainly aimed at participating students and junior researchers and will have essentially the character of a summer school. On Wednesday afternoon the more advanced part of the conference will start. In this framework links of a foundational theory and computer implementations will be discussed and we will compare set theory and homotopy type theory regarding their role as a foundation of mathematics. Finally on Saturday there will be a philosophical satellite workshop regarding the topic of revolutions in mathematics.

​Schedule

Monday, July 18

1:00 - 2:00 pm
2.00 - 3:30 pm

​3:30 - 4:00 pm
​4:00 - 5:30 pm

​5:30 - 7:00 pm


7:00 pm -
Opening
Vladimir Voevodsky
Multiple Concepts of Equality in the New Foundations of Mathematics
Tea break
Marc Bezem
"Elements of Mathematics" in the Digital Age
Parallel Workshop Session​​
A) Ioanna Dimitriou: Formalising Set Theoretic Proofs with Isabelle/HOL in Isar
B) Regula Krapf: Introduction to Forcing
Light Dinner

Tuesday, July 19

9:00 - 10:30 am

​10:30 - 11:00 am
​11:00 am - 12:30 pm

12:30 - 2.00 pm
​2:00 - 3:30 pm


​3:30 - 4:00 pm
4:00 - 5:30 pm

5:30 - 7:00 pm


​​7:00 pm -
Thorsten Altenkirch
Naïve Type Theory
Tea break
Benedikt Ahrens
Univalent Foundations and the Equivalence Principle
Lunch
Parallel Workshop Session​​
​A) Ioanna Dimitriou: Formalising Set Theoretic Proofs with Isabelle/HOL in Isar
B) Regula Krapf: Introduction to Forcing
​Tea Break
Clemens Ballarin
​Structuring Mathematics in Higher-Order Logic
Parallel Workshop Session​​
A) Ulrik Buchholtz: Higher Inductive Types and Synthetic Homotopy Theory
B) Paige North: Models of Type Theory
Light Dinner

Wednesday, July 20

9:00 - 10:30 am


​10:30 - 11:00 am
​11:00 am - 12:30 pm

​
​12:30 - 2.00 pm
​2:00 - 3:30 pm

​
3:30 - 4:00 pm
4:00 - 5:30 pm

5:30 - 7:00 pm
​
​7:00 - 8:00 pm
8:00 pm -
Parallel Workshop Session​​
​A) Clemens Ballarin: Proof Assistants (Isabelle) I
B) Alexander C. Block: Modal Logic of Forcing
​Tea Break
Parallel Workshop Session​​
​A) Clemens Ballarin: Proof Assistants (Isabelle) II
B) Ulrik Buchholtz: Higher Inductive Types and Synthetic Homotopy Theory
​Lunch
Parallel Workshop Session
A) Alexander C. Block: Modal Logic of Forcing
​B) Paige North: Models of Type Theory
Tea Break
Thomas Streicher
Isomorphic Types are Equal!?
Claudio Ternullo
Multiversism and Naturalism
Light Dinner
Plenum & Ad Hoc Meetings*

Thursday, July 21

9:00 - 10:00 am
​
​10:00 - 11:00 am

​11:00 - 11:30 am
11:30 am - 12:30 pm
​
​12:30 - 2:00 pm
​2:00 - 3:00 pm
​

3:00 - 3:30 pm
​3:30 - 5:30 pm

​
5:30 - 7:00 pm
​7:00 pm -
Michael Rathjen
​Relating Type and Set Theories
Andrew Pitts
On Proofs of Equality as Paths
​Tea Break
Bas Spitters
​Sets in Homotopy Type Theory
​Lunch
​Mirna Džamonja
​A new look at an Old Lady: Modern Set Theory and its Place in the Foundations of Mathematics
Tea Break
Panel Discussion: Mathematical Aspects
Moderator: Thomas Streicher
​Panelists: Mirna Džamonja, Andrew Pitts, Michael Rathjen, Bas Spitters
Plenum & Ad Hoc Meetings*
Conference Dinner

Friday, July 22

9:00 - 10:00 am
​
​10:00 - 11:00 am

​11:00 - 11:30 am
11:30 am - 12:30 pm
​
​12:30 - 2:00 pm
​2:00 - 3:00 pm
​
3:00 - 3:30 pm
​3:30 - 5:30 pm

​
5:30 - 5:45 pm
5:45 - 7:00 pm
​
7:00 pm -
​
Ulrik Buchholtz
Proof Theory of Homotopy Type Theories
Nathan Bowler
Borel Determinacy and Infinite Graphs
Tea Break
​James Ladyman
Does HoTT Provide a Foundation for Mathematics?
Lunch
Philip Welch
Proving Theorems from Reflection
​Tea Break
Panel Discussion: Philosophical Aspects
Moderator: Benedikt Löwe
​Panelists: Thorsten Altenkirch, James Ladyman, Andrei Rodin, Philip Welch
​Break
Urs Schreiber - informal session
The nLab
Light Dinner

Saturday, July 23

9:00 - 10:00 am
​
​10:00 - 11:00 am
​
​11:00 - 11:30 am
11:30 am - 12:30 pm
​
​12:30 - 1:30 pm
1:30 - 2:30 pm

2:30 - 3:00 pm
Benedikt Löwe
​Multiverse Truth Behaviour Patterns
Urs Schreiber
​Modern Physics Formalized in Modal Homotopy Type Theory
Tea Break
Ioanna Dimitriou
Formalising a FOL Set Theory in Isabelle/HOL, in a Textbook Fashion​
Snacks
Andrei Rodin
Proofs and Objects in HoTT 
Closing Session

​*What are Ad Hoc Meetings?

Ad hoc Meetings are a new form of conference activity. The idea is to provide a framework in which participants can meet in smaller groups and discuss research topics which spontaneously came up during previous presentations or discussions at the conference.
In a short plenum at the beginning of each Ad Hoc Meeting slot, participants can propose topics (with a short and precise description thereof) which will be collected by the organisors. In a quick vote the proposals with the most interested participants will be determined and subsequently assigned rooms in which these 'ad hoc groups' can discuss the respective topics.