Normalization in type theory: where it is needed, and where not

Iowa Type Theory Commute

Normalization (every term reaches a normal form via some reduction sequence) is needed essentially in type theory due to the Curry-Howard isomorphism: diverging programs become unsound proofs. Traditionally, type theorists have also desired normalization or even termination (every term reaches a normal form no matter what reduction sequence is explored in a nondeterministic operational semantics) for conversion checking. This is the process of confirming that types are equivalent during type checking, which, due to dependent types, can require checking program equivalence. The latter is usually restricted to just beta-equivalence (where beta-reduction is substitution of argument for input variable when applying a function), because richer notions of program equivalence are usually undecidable. I have a mini-rant in this episode explaining why this usual requirement of normalization for conversion checking is not sensible.
Also I note that you can find the episodes of the podcast organized by chapter on my web page.