College of Science & Engineering
Twin Cities
Type theory has been the foundation of many interactive theorem provers used to verify the correctness of software and mathematical proofs. Recent research revealed a novel way of applying type theory to homotopy theory, the study of topological spaces up to continuous deformation. The idea is to equip type-theoretic constructs with higher-dimensional structure so that they can capture homotopy-theoretic structure. This feature gave rise to a new field homotopy type theory and has led to a significant amount of mechanization of homotopy theory.
These researchers would like to further improve the theory and tools based on higher-dimensional structure, to facilitate mechanizing results in mathematics and computer science. In particular, there are significant examples that, in the improved theories, can be automatized entirely. The resources at MSI enable testing of the prototypes in more challenging cases.