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

该项目支持20名学生和博士后研究人员参加将于2023年5月22日至25日在匹兹堡卡内基梅隆大学举行的第二届同伦类型理论国际会议。 同伦类型理论是数学的一个新领域，它借鉴了多个学科，包括逻辑，同伦理论，范畴理论和计算机科学。它与新的计算机化证明助手的发展密切相关，这些助手允许交互式地构建数学证明并验证其正确性。 同伦类型理论是基于最近发现的构造型理论、同伦理论和高等范畴理论之间的联系，它是一门基于构造型理论、同伦理论和高等范畴理论之间的联系的理论。 马丁-洛夫的依赖类型理论是一个形式化的系统，支持Lean、Coq和Agda等计算机化的证明助手。 这个系统最近被证明可以解释为某些最初为同伦理论开发的更高类别。 因此，它也可以用于高等数学中的推理。 重要的是，基于它的证明助手可以用于正式验证这些领域的困难结果，而这些结果是以前这些工具无法实现的。 新应用程序对系统的扩展也大大扩展了可以使用证明助手开发和形式化的数学范围。会议网站：https://hott.github.io/HoTT-2023This奖反映了NSF的法定使命，并已被认为值得通过使用基金会的知识价值和更广泛的影响审查标准进行评估的支持。

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