I was learning about type systems from Benjamin C. Pierce’s Types and Programming Languages and came across the Lambda cube in the chapter on Higher-Order Polymorphism. After reading up more about it on Wikipedia I learnt about its generalization, Pure type system where it is mentioned that
It is a major open problem in the field whether this is always the case, i.e. whether a (weakly) normalizing PTS always has the strong normalization property.This is known as the Barendregt–Geuvers–Klop conjecture.
However, I am unable to think of practical applications of a proof (or disproof) of the above conjecture (perhaps due to my limited knowledge of type theory).
Question: What are the practical applications of a proof (or disproof) of the Barendregt–Geuvers–Klop conjecture?