CMU-CS-21-100Computer Science Department School of Computer Science, Carnegie Mellon University
CMU-CS-21-100
Evan Cavallo Ph.D. Thesis February 2021
Keywords:
Dependent type theory, computational semantics, cubical type theory, internal parametricity, cohesive type theory
Recent innovation in the design of type theories–foundational systems of mathematics with a focus on constructivity–has produced the concept of interval variable, which can be used to capture relations between objects that carry computational content. We examine two such relationships in type theory: equality, in particular quotients, and arbitrary relations as applied in parametricity interpretations. Cubical type theory, a system using an interval-based formulation of equality, enables a permissive kind of content-carrying equality that includes in particular isomorphism. Cubical type theory provides a constructive interpretation of homotopy type theory and the Univalent Foundations, formalisms that introduced the idea of isomorphism as equality but which lack intrinsic computational meaning. The cubical approach to equality also rectifies long-standing deficiencies in the behavior of quotients in type theory. We realize a system of generalized quotients for cubical type theory originally conceived in homotopy type theory, called higher inductive types, that merges the concepts of inductive type and quotient. Such a mutual generalization is particularly essential in the contentful equality setting, but also has significant applications to ordinary mathematics. Parametricity is, among other things, a proof technique for deriving properties of constructions performed in type theories, based on the idea that constructions preserve all relations between objects. Traditionally a meta-theoretical tool, recent work has shown that parametricity properties can be integrated into a type theory itself using an interval-based system. We develop internal parametricity on top of cubical type theory, examining the similarities and distinctions between the two applications of intervals, finding that a background of cubical equality improves the behavior of internal parametricity, and applying internal parametricity as a tool to solve difficult problems in cubical type theory. We introduce a system of cohesion modalities to express the interaction between parametric and non-parametric type theory, enabling the use of parametricity results in a non-parametric setting. 322 pages
Srinivasan Seshan, Head, Computer Science Department
| |

Return to:
SCS Technical Report Collection This page maintained by reports@cs.cmu.edu |