CMU-CS-19-127 Computer Science Department School of Computer Science, Carnegie Mellon University
Computational Semantics of Cartesian Cubical Type Theory Carlo Angiuli Ph.D. Thesis September 2019
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:
Srinivasan Seshan, Head, Computer Science Department
| |
Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |