- (27 Aug)
- (28 Aug)
- (29 Aug)
To kick off the new academic year, project leaders Marc Bezem and Bjørn Ian Dundas invite their fellows to join them for a three-day seminar.
During this seminar, the fellows participating in the CAS project Homotopy Type Theory and Univalent Foundations will introduce themselves and their work, as well as discuss their plans and goals during their one-year stay at CAS.
Attendence by invitation only.
About the project:
What is a proof? And what does it mean to be equal?
The answers to these questions vary enormously, both through time, but also from one culture to another. The modern mathematical proof may seem the most rigorous of all alternatives. Still, the ideal of well-documented, accountable knowledge, communicated with a proof certificate, is in no way reached. Typically, the validity of extremely complicated mathematical proofs is still supported only by the community's trust in peer review performed by a few acknowledged experts.
Since modern society depends on mathematics, secure foundations are important. In the digital era we have powerful tools for verifying (and to some extent generating) formal mathematical proofs. The central challenge is finding a language that has sufficient expressive power and at the same time can be mechanically processed in an efficient way. Homotopy type theory addresses exactly this challenge.
In this approach equality has a topological interpretation, yielding great flexibility. Our project aims to further explore this novel foundation of mathematics, and apply it to verify some challenging mathematical theories.
09.30-10.30 BJØRN IAN DUNDAS, University of Bergen, & CAMILLA SERCK-HANSSEN, Scientific Director of CAS
- Welcome to the CAS Year on Homotopy Type Theory and Univalent Foundations
10.45-11.45 CHRISTIAN SATTLER, University of Gothenburg
- A Constructive Perspective on Homotopical Algebra Using (Marked) Semisimplicial Sets
14.00-15.00 BENEDIKT AHRENS, University of Birmingham
- A Type Theory of Type Theories
15.30-16.30 DANIEL GRAYSON, University of Illinois at Urbana-Champaign
- Some Projects I’d Like to Work On
- Monoidal Structures and Formalization of Coherence Theorems
- The Barratt-Priddy-Quillen Theorem in Homotopy Type Theory
10.45-11.45 ULRIK BUCHHOLTZ, Technical University Darmstadt
- Model Structures on Cubical Sets
14.00-15.00 PETER LEFANU LUMSDAINE, Stockholm University
- Towards a General Meta-Theory of Type Theories
15.30-16.30 KUEN-BANG HOU (FAVONIA), University of Minnesota
09.30-10.30 FLORIS VAN DOORN, Carnegie Mellon University
- Spectral Sequences in Homotopy Type Theory
10.45-11-45 THIERRY COQUAND, Chalmers / University of Gothenburg
14.00-15.00 PETER DYBJER, Chalmers / University of Gothenburg
- Internal Type Theory Revisited
15.30-16.30 MARC BEZEM, University of Bergen
- Experiences with Teaching Homotopy Type Theory