Proofs of the normalization and Church-Rosser theorems for the typed $\lambda$-calculus.
Garrel Pottinger · Notre Dame Journal of Formal Logic · 1978
GARREL POTTINGER1.It is not shown that every reduction sequence must contain a normal term.2. Rubin [l,pp.175-219] is enough.3. The use/mention conventions of Curry will be employed-all symbols written down are in the metalanguage and the objectlanguage is never displayed.