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 类型理论通过承认依赖类型和项来扩展 lambda 演算，并且至少与二阶逻辑一样强大。由于它结合了表达能力和理想的证明理论属性，它也被用作几种高级编程语言的基础。使用 Quillen 模型类别的框架并依赖于涉及（弱）高维群群的相关代数方法，将该系统解释为公理同伦理论。 这使得逻辑方法能够与代数和拓扑方法相结合，允许类型论在同伦和高维代数中的理论和计算应用。这项研究追求几何、代数和逻辑之间令人惊讶的联系，这种联系是由 PI 发现的，目前正在由世界各地的几位研究人员积极研究。除了在数学基础中的重要性之外，它还具有在计算机科学中直接应用的巨大潜力。 所研究的逻辑系统广泛用于编程语言的设计和实现。 新的几何和代数解释既可用于确保应用系统的正确性，又可作为此类系统实现的计算范式的理论模型。 相反，逻辑系统的发达计算实现使得几何和代数中的计算应用成为可能。 该研究的更广泛影响体现在科学技术应用和研究生教育方面。 卡内基梅隆大学纯粹与应用逻辑项目的一名博士生得到了该研究项目的部分支持。 学生正在接受逻辑、拓扑和代数相关领域的培训，并与 PI 进行联合研究，最终获得博士学位。