Normalization for simply-typed \lambda-calculus

As explained in its main page, normalization for type theories can be given in two ways:

normalization through rewriting (often known as weak or strong normalization, depending on how deep into a term it goes)
normalization by evaluation (which uses more semantic approaches)

This page is about proving normalization for the simply-typed \lambda-calculus. As a result, it was first obtained by Tait 1967. However, there have been many other approaches since.

Normalization through rewriting

Please expand.

Normalization by Evaluation

Please expand.

References

Tait, W. W. 1967. ‘Intensional Interpretations of Functionals of Finite Type I’. Journal of Symbolic Logic 32 (2): 198–212. https://doi.org/10.2307/2271658.

@article{tait_intensional_1967,
	title = {Intensional {Interpretations} of {Functionals} of {Finite} {Type} {I}},
	volume = {32},
	doi = {10.2307/2271658},
	number = {2},
	journal = {Journal of Symbolic Logic},
	author = {Tait, W. W.},
	year = {1967},
	pages = {198--212}
}