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

Andreas Abel; Thierry Coquand

doi:10.23638/LMCS-16(2:14)2020

Andreas Abel ; Thierry Coquand - Failure of Normalization in Impredicative Type Theory with Proof-Irrelevant Propositional Equality

lmcs:6068 - Logical Methods in Computer Science, June 30, 2020, Volume 16, Issue 2 - https://doi.org/10.23638/LMCS-16(2:14)2020

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

Authors: Andreas Abel ; Thierry Coquand

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].

https://doi.org/10.23638/LMCS-16(2:14)2020

Source: arXiv.org:1911.08174

Volume: Volume 16, Issue 2

Published on: June 30, 2020

Accepted on: June 3, 2020

Submitted on: February 3, 2020

Keywords: Computer Science - Logic in Computer Science,Computer Science - Programming Languages,Mathematics - Logic

Licence: Attribution 4.0 International (CC BY 4.0)