Homotopy and Type Theory

Carnegie Mellon University, Pittsburgh PA

Investigators

Abstract

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.