Workshop on Homotopy Type Theory and Univalent Foundations of Mathematics
Speakers
Details
Homotopy Type Theory is a new area of research, combining ideas from homotopy theory (a branch of topology) and dependent type theory (a formal system studied in mathematical logic and theoretical computer science). It is based on the realization that the logical notion of equality between two objects can carry more information beyond its truth value and as such may resemble the notion of homotopy between two continuous maps. The workshop will consist of mini-courses in the mornings and research-level talks (invited and contributed) in the afternoons. As such, it is meant as a venue for both the experts in the field and researchers from related areas interested in learning more about Homotopy Type Theory.
Additional Information
For complete information on registration, travel arrangements and abstract submission, please visit the conference website.
Mini-courses
Robert Harper (Carnegie Mellon University): Computational Higher Type Theory
Daniel R. Licata (Wesleyan University): Cubical Type Theory
Peter LeFanu Lumsdaine (Stockholm University): Homotopy-theoretic models of type theory
Michael Shulman (University of San Diego): Synthetic Homotopy Theory
Invited speakers
Benedikt Ahrens (IAS, Princeton)
Thorsten Altenkirch (University of Nottingham)
Jeremy Avigad (Carnegie Mellon University)
Emily Riehl (Johns Hopkins University)
Michael Warren (HRL Laboratories)
