Michael Shulman Receives Subcontract with Carnegie Mellon University

Michael Shulman, PhD Mathematics, received a $28,659 subcontract with Carnegie Mellon University with the prime funding coming from the United States Air Force Research Laboratory. The purpose of this research is to study univalent models of type theory using semantic category-theoretic methods, particularly their generalizations to include higher inductive types, and whether algorithms for computing with univalence can be extracted from such models. The research involves collaboration with Carnegie Mellon University in order to design new type theories as well as develop and formalize the mathematics in these new foundational systems.