Computer Science Speaking Skills Talk

  • Gates Hillman Centers
  • Traffic21 Classroom 6501
  • CARLO ANGIULI
  • Ph.D. Student
  • Computer Science Department
  • Carnegie Mellon University
Speaking Skills

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

For More Information, Please Contact: 
Keywords: