Dependent type theories are a family of logical systems that serve as expressive functional programming languages and as the basis of many proof assistants. In the past decade, type theories have also attracted the attention of mathematicians due to surprising connections with homotopy theory; the study of these connections, known as homotopy type theory, has in turn suggested novel extensions to type theory, including higher inductive types and Voevodsky’s univalence axiom. However, in their original axiomatic presentation, these extensions lack computational content, making them unusable as programming constructs and unergonomic in proof assistants.

In this dissertation, we present Cartesian cubical type theory a univalent type theory that extends ordinary type theory with interval variables representing abstract hypercubes. We justify Cartesian cubical type theory by means of a computational semantics that generalizes Allen’s semantics of Nuprl [All87] to Cartesian cubical sets. Proofs in our type theory have computational content, as evidenced by the canonicity property that all closed terms of Boolean type evaluate to true or false. It is the second univalent type theory with canonicity, after the De Morgan cubical type theory of Cohen et al. [CCHM18], and armatively resolves an open question of whether Cartesian interval structure constructively models univalent universes.

187 pages

Thesis Committee:
Robert Harper (Chair)
Jeremy Avigad
Karl Crary
Kuen-Bank Hou (Favonia) (University of Minnesota)
Daniel R. Licata (Wesleyan University)
Todd Wilson (California State University, Fresno)

Srinivasan Seshan, Head, Computer Science Department
Martial Hebert, Dean, School of Computer Science

Return to: SCS Technical Report Collection
School of Computer Science

This page maintained by [email protected]