College of Science & Engineering
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 each type-theoretic construct with higher-dimensional structure so that homotopy-theoretic structure may be captured by type theory. This 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, in order to facilitate mechanizing results in mathematics and computer science. In particular, they have several important examples that, in the improved theories, can be completely automatized or largely simplified. The resources at MSI enable testing of the prototypes on more challenging examples.