Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality
From MaRDI portal
Publication:6329469
arXiv1911.08174MaRDI QIDQ6329469FDOQ6329469
Authors: Andreas Abel, Thierry Coquand 
Publication date: 19 November 2019
Abstract: Normalization fails in type theory with an impredicative universe of propositions and a proof-irrelevant propositional equality. The counterexample to normalization is adapted from Girard's counterexample against normalization of System F equipped with a decider for type equality. It refutes Werner's normalization conjecture [LMCS 2008].
This page was built for publication: Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6329469)
