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