New Mathematics of Information: Homotopical and Higher Categorical Foundations of Information and Computation.

摘要

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.