Weak normalization implies strong normalization in pure type systems
What the paper claims, in its own words
Proves that weak normalization implies strong normalization for every pure type system: if every legal expression in every valid context has a β-normal form, every β-reduction sequence terminates. This resolves the β-Barendregt–Geuvers–Klop conjecture, including nonfunctional rules and open contexts.
The plain-language explainer for this entry is still coming.
The original paper
- Weak and strong normalization in pure type systems (PDF, opens in a new tab) September 25, 2026