You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.
Jon Sterling (Apr 01 2021 at 12:08):I'm very happy to be able to confirm that the paper "Normalization for Cubical Type Theory" by Carlo Angiuli and myself has been accepted to LICS this year. You can see our preprint here: http://www.jonmsterling.com/pdfs/cubical-norm.pdf
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 an injective function from equivalence classes of terms in context to a tractable language of β/η-normal forms. As corollaries we obtain both decidability of judgmental equality as well as the injectivity of type constructors in judgmentally consistent contexts.