Conference: Student Support for Second International Conference on Homotopy Type Theory (HoTT 2023)

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

This project supports attendance by 20 students and postdoctoral researchers at the Second International Conference on Homotopy Type Theory, to be held 22–25 May 2023 at Carnegie Mellon University in Pittsburgh. Homotopy type theory is a new field of Mathematics that draws on multiple disciplines, including logic, homotopy theory, category theory, and computer science. It is closely tied to the development of new computerized proof assistants that permit mathematical proofs to be constructed interactively and verified to be correct. Student participants will learn about both the theory and practice of such computational tools, which are becoming increasingly important in the exact sciences. Homotopy type theory is based on recently discovered connections between constructive type theory, homotopy theory, and higher category theory. Martin-Löf’s dependent type theory is a formal system that underlies computerized proof assistants such as Lean, Coq, and Agda. This system was recently shown to interpret into certain higher-categories originally developed for homotopy theory. As a result, it can also be used for reasoning in higher mathematics. Importantly, the proof assistants based on it can then be used to formally verify difficult results in these areas not previously attainable by such tools. Extensions to the system suggested by the new applications also greatly extend the range of mathematics that can be developed and formalized using proof assistants. Conference website: https://hott.github.io/HoTT-2023 This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.