Strong normalization proof with CPS-translation for second order classical natural deduction
Koji Nakazawa, Makoto Tatsuta · Journal of Symbolic Logic · 2003
Abstract This paper points out an error of Parigot's proof of strong normalization of second order classical natural deduction by the CPS-translation, discusses erasing-continuation of the CPS-translation, and corrects that proof by using the notion of augmentations.