Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality
Logic in Computer Science
2023-06-22 v4 Programming Languages
Logic
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].
Cite
@article{arxiv.1911.08174,
title = {Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality},
author = {Andreas Abel and Thierry Coquand},
journal= {arXiv preprint arXiv:1911.08174},
year = {2023}
}