Workshop on Homotopy Type Theory and Univalent Foundations of Mathematics

  • Start Date: 05/16/2016
  • End Date: 05/20/2016
Speaker(s):

 

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)

Location: 

University of Toronto

Description: 

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.

Organizers:

J. Daniel Christensen (University of Western Ontario)

John F. Jardine (University of Western Ontario)

Chris Kapulkin (University of Western Ontario)

Other Information: 

For complete information on registration, travel arrangements and abstract submission, please visit  the conference website.

Sponsor: