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.

该项目支持2023年5月22日至25日在匹兹堡的卡内基·梅隆大学举行的第二次国际同型类型理论会议上的20名学生和博士后研究人员的出勤。同型类型理论是一个新的数学领域，它借鉴了多个学科，包括逻辑，同义理论，类别理论和计算机科学。它与新的计算机证明助理的开发密切相关，这些助理允许互动构造数学证明并确认为正确。学生参与者将了解此类计算工具的理论和实践，这些计算工具在确切的科学中变得越来越重要。Homotopy类型理论基于最近发现的建设性类型理论，同义理论和更高类别理论之间的联系。 Martin-Löf的依赖类型理论是一种正式的系统，其基础是计算机证明助手，例如Lean，Coq和Agda。最近显示，该系统将解释为最初用于同型理论的某些高级类别。结果，它也可以用于更高数学的推理。重要的是，可以使用基于它的证明助手来正式验证这些工具以前无法实现的这些领域的困难结果。新应用程序建议的系统的扩展也很大程度上扩展了可以使用证明助手开发和形式化的数学范围。会议网站：https：//hott.github.io/hott-2023 This Award反映了NSF的法定任务，并使用基金会的知识分子优点和更广泛的影响审查标准，认为通过评估被认为是珍贵的支持。