Strong normalization from weak normalization in typed \(\lambda\)-calculi (Q1357009): Difference between revisions

For some typed \(\lambda\)-calculi it is easier to prove weak normalization than strong normalization. Techniques to infer the latter from the former have been invented but they infer strong normalization of one notion of reduction from weak normalization of a more complicated notion of reduction. The paper presents a new technique to infer strong normalization from weak normalization of the same notion of reduction. This is demonstrated by examples including System F.