New Mathematics of Information: Homotopical and Higher Categorical Foundations of Information and Computation
Final rept. 15 Jun 2011-30 Apr 2014
CARNEGIE-MELLON UNIV PITTSBURGH PA
Pagination or Media Count:
The research funded by this award introduced a new paradigm in informatics based on a new mathematical analysis of computation. It employed a connection between Geometry, Algebra, and Logic via an interpretation of constructive type theory into homotopy theory, discovered around 2005 by the PI and his students. In addition to its intrinsic mathematic importance, this connection has resulted in a new geometry of computation. Powerful machine implementations of type theory in the form of proof assistants already permit partial automation of reasoning in such systems under the new homotopical interpretation, such formal reasoning can encompass abstract programming languages, constructive mathematics, and large swaths of classical mathematics, including systems as powerful as ZF set theory. The work was pursued at the Institute for Advanced Study Princeton in 2012-13 in a program co-organized by the PI. A group of leading logicians, computer scientists, and mathematicians developed algorithms to support the new foundations, furthering its applications to pure and applied mathematics and computation, and enhanced existing proof assistants to implement them. This work will lead to the wide-spread use of computational proof assistants, large-scale formalization of mathematics, and the creation of powerful scientific tools with impact on challenging problems of DoD interest.
- Theoretical Mathematics