As explained in its main page, normalization for type theories can be given in two ways:
This page is about proving normalization for the simply-typed -calculus. As a result, it was first obtained by [Tait 1967]. However, there have been many other approaches since.
Please expand.
Please expand.
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}
}