![]() |
![]() |
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].
Source : ScholeXplorer
IsCitedBy DOI 10.4230/lipics.types.2021.6
Donkó, István ; Kaposi, Ambrus ; |