Homotopy and Type Theory

同伦与类型论

• 批准号: 1001191
• 负责人: Steven Awodey
• 金额: $ 24.29万
• 依托单位: Carnegie-Mellon University
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2010
• 资助国家: 美国
• 起止时间: 2010-08-01 至 2013-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1001191&HistoricalAwards=false
• 关键词: Homotopy; Type; Theory

A recently-discovered connection between the constructive type theory and homotopy theory is investigated using the tools of higher- dimensional algebra. Martin-Lof type theory extends the lambda- calculus by admitting dependent types and terms, and is at least as strong as second-order logic. It is also used as the basis of several high-level programming languages because of its combination of expressive strength and desirable proof-theoretic properties. The system is interpreted into axiomatic homotopy theory using the framework of Quillen model categories and relying on related algebraic methods involving (weak) higher-dimensional groupoids. This permits logical methods to be combined with algebraic and topological ones, admitting theoretical and computational applications of type theory in homotopy and higher-dimensional algebra.This research pursues a surprising connection between Geometry, Algebra, and Logic which was discovered by the PI and is now under active investigation by several researchers worldwide. In addition to its importance in foundations of mathematics, it has strong potential for direct applications in computer science. Logical systems of the kind investigated are used extensively in programming language design and implementation. The new geometric and algebraic interpretations are of use both in securing the correctness of applied systems and as a theoretical model of the computational paradigms implemented by such systems. Conversely, computational applications in geometry and algebra are made likely by the well-developed computational implementations of the logical system. The broader impact of the research is both in applications in science and technology and in graduate education. A doctoral student in Carnegie Mellon's Pure and Applied Logic program is partially supported under this research project. The student is being trained in the relevant areas of logic, topology, and algebra, and conducts joint research with the PI, eventually leading to the degree of PhD.

利用高维代数的工具研究了构造型理论与同伦理论之间的联系。Martin-Lof类型理论通过承认依赖类型和项扩展了λ演算，并且至少与二阶逻辑一样强大。它还被用作一些高级编程语言的基础，因为它结合了表达能力和理想的证明理论性质。利用Quillen模型范畴的框架，依靠涉及（弱）高维群的相关代数方法，将该系统解释为公理化同伦理论。这允许逻辑方法与代数和拓扑方法相结合，承认类型论在同伦和高维代数中的理论和计算应用。这项研究追求几何、代数和逻辑之间的惊人联系，这种联系是由PI发现的，现在正在由世界各地的几位研究人员积极研究。除了它在数学基础中的重要性外，它在计算机科学中的直接应用也具有强大的潜力。所研究的逻辑系统广泛应用于程序设计语言的设计和实现。新的几何和代数解释既可用于确保应用系统的正确性，也可作为由此类系统实现的计算范式的理论模型。相反，几何和代数中的计算应用可能是由逻辑系统的良好开发的计算实现实现的。研究的更广泛的影响是在科学和技术的应用和研究生教育。卡内基梅隆大学纯逻辑与应用逻辑项目的一名博士生在本研究项目下获得部分资助。该学生正在接受逻辑学、拓扑学和代数等相关领域的培训，并与PI进行联合研究，最终获得博士学位。