Normalization for Cubical Type Theory

Abstract

We prove normalization for (univalent, Cartesian) cubical type theory, closing the last major open problem in the syntactic metatheory of cubical type theory. Our normalization result is reduction-free, in the sense of yielding a bijection between equivalence classes of terms in context and a tractable language of $\beta /\eta$-normal forms. As corollaries we obtain both decidability of judgmental equality and the injectivity of type constructors.

LICS 2021

References in corpus (4)

• Normalization for Cubical Type Theory
• Using the internal language of toposes in algebraic geometry
• A Cubical Language for Bishop Sets
• Syntactic categories for dependent type theory: sketching and adequacy

Cited by in corpus (7)

• Normalization for Cubical Type Theory
• A Cubical Language for Bishop Sets
• Relative induction principles for type theories
• On the $\infty$-topos semantics of homotopy type theory
• A cost-aware logical framework
• Logical Relations as Types: Proof-Relevant Parametricity for Program Modules
• Controlling unfolding in type theory