Computing with univalence in Cartesian cubical type theory
Dependent type theories, such as those underlying the proof assistants Coq, Agda, and Nuprl, are simultaneously theories of constructive mathematics and of computer programming: a proof of a proposition is at the same time a program that executes according to a specification. In the past decade, mathematicians have uncovered a surprising interpretation of types as abstract topological spaces, leading to extensions of type theory known as higher inductive types and the univalence axiom. Unfortunately, as originally formulated, these extensions disrupt the computational nature of proofs.
We will describe Cartesian cubical type theory, a novel dependent type theory that supports higher inductive types and univalence while restoring the connection between proofs and programs. We will also demonstrate how univalence can simplify ordinary type-theoretic reasoning in the RedPRL proof assistant currently under development at CMU.
Joint work with Kuen-Bang Hou (Favonia) and Robert Harper.
Presented in Partial Fulfillment of the CSD Speaking Skills Requirement