一句话：构造反例证明带证明无关命题等式的非直谓类型论不满足归一化，反驳 Werner 猜想。
本文研究非直谓命题宇宙与证明无关命题等式并存时类型论的归一化性质。作者将 Girard 针对带有类型相等判定器的 System F 的归一化反例加以改造，构造出在该类型论中破坏归一化的项，从而证明归一化不可用。该结果构成 Werner 在 LMCS 2008 中提出的归一化猜想的反例，说明在这些假设下不能期望所有项归约到范式，也揭示了证明无关等式与非直谓性组合的证明论强度。
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].
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{AbelC20,
title = {Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality},
author = {Andreas Abel and Thierry Coquand},
journal = {Logical Methods in Computer Science},
volume = {Volume 16, Issue 2},
year = {2020},
doi = {10.23638/lmcs-16(2:14)2020}
}