Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality
Andreas Abel, Thierry Coquand
TL;DR
This paper demonstrates that normalization does not hold in a specific impredicative type theory with proof-irrelevant propositional equality, providing a counterexample that challenges previous assumptions.
Contribution
It presents a counterexample showing the failure of normalization in impredicative type theory with proof-irrelevant equality, refuting Werner's conjecture.
Findings
Normalization fails in the specified type theory
Counterexample adapted from Girard's work
Refutes Werner's normalization conjecture
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].
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.