Univalence from a computer science point-of-view

Abstract: One formal system for Voevodsky's univalent foundations is Martin-Löf's type theory. This type theory is the basis of proof assistants, such as Agda, Coq, and NuPRL, that are used not only for the formalization of mathematics, but in computer science for verification of programs, systems, and programming language designs and implementations. These applications rely on the fact that constructions in type theory can be interpreted constructively as programs. Voevodsky's introduction of the univalence axiom was thus exciting from a computer science point view, because it suggested new programs that could be added to type theory, and new principles that could be used in program verification. However, for such applications, it is necessary to know that the addition of univalence preserves the computational character of type theory, which is Voevodsky's homotopy canonicity conjecture. While homotopy canonicity has not yet been proved as stated, this problem has led to a great deal of research aimed at understanding the computational meaning of univalence. This has resulted in several new constructive models of univalent foundations, and new type theories and programming languages based on them. In this talk, I will give a high-level survey of the motivations for, challenges of, current knowledge about, and applications of work on this problem.