Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality

November 19, 2019 · The Ethereal · 🏛 Log. Methods Comput. Sci.

🔮 THE ETHEREAL: The Ethereal
Pure theory — exists on a plane beyond code

"No code URL or promise found in abstract"

Evidence collected by the PWNC Scanner

Authors Andreas Abel, Thierry Coquand arXiv ID 1911.08174 Category cs.LO: Logic in CS Cross-listed cs.PL, math.LO Citations 16 Venue Log. Methods Comput. Sci. Last Checked 2 months ago
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].
Community shame:
Not yet rated
📄 View on arXiv 🌐 View on ar5iv 📑 PDF 🎉 Report Code Found
Community Contributions

Found the code? Know the venue? Think something is wrong? Let us know!

📜 Similar Papers

In the same crypt — Logic in CS