Strong normalization proof with CPS-translation for second order classical natural deduction

Nakazawa, Koji; Tatsuta, Makoto

J. Symbolic Logic, Tome 68 (2003) no. 1, p. 851- 859 / Harvested from Project Euclid

Résumé

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.

Publié le : 2003-09-14
Classification:

@article{1058448444,
     author = {Nakazawa, Koji and Tatsuta, Makoto},
     title = {Strong normalization proof with CPS-translation for second order classical natural deduction},
     journal = {J. Symbolic Logic},
     volume = {68},
     number = {1},
     year = {2003},
     pages = { 851- 859},
     language = {en},
     url = {http://dml.mathdoc.fr/item/1058448444}
}

Nakazawa, Koji; Tatsuta, Makoto. Strong normalization proof with CPS-translation for second order classical natural deduction. J. Symbolic Logic, Tome 68 (2003) no. 1, pp.  851- 859. http://gdmltest.u-ga.fr/item/1058448444/