Homotopy and Type Theory

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

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.