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进行联合研究，最终获得博士学位。