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

会议：第二届同伦类型理论国际会议 (HoTT 2023) 的学生支持

• 批准号: 2318492
• 负责人: Steven Awodey
• 金额: $ 2.4万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-04-01 至 2024-03-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2318492&HistoricalAwards=false
• 关键词: Conference; Student; Support; Second; International

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.

该项目支持 20 名学生和博士后研究人员参加将于 2023 年 5 月 22 日至 25 日在匹兹堡卡内基梅隆大学举行的第二届同伦类型理论国际会议。它与新的计算机化证明助手的开发密切相关，这些助手允许交互地构建数学证明并验证其正确性。参与者将了解此类计算工具的理论和实践，这些工具在精确科学中变得越来越重要。同伦类型理论基于最近发现的构造类型理论、同伦理论和更高的 Martin-Löf 依赖范畴论之间的联系。类型理论是一种形式系统，是 Lean、Coq 和 Agda 等计算机化证明助手的基础。该系统最近被证明可以解释最初为同伦理论开发的某些更高类别。因此，它也可以用于推理。重要的是，基于它的证明助手可以用来正式验证这些领域中以前无法通过此类工具获得的结果。新应用程序建议的系统扩展也极大地扩展了数学的范围。使用证明助理开发和正式化。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。