Paper: Strong normalization for second order classical natural deduction (at LICS 1993)
Authors: Michel ParigotAbstract
The strong normalization theorem for second-order classical natural deduction is proved. The method used is an adaptation of the one of reducibility candidates introduced in a thesis by J.Y. Girard (Univ. Paris 7, 1972) for second-order intuitionistic natural deduction. The extension to the classical case requires, in particular, a simplification of the notion of reducibility candidates
BibTeX
@InProceedings{Parigot-Strongnormalization, author = {Michel Parigot}, title = {Strong normalization for second order classical natural deduction }, booktitle = {Proceedings of the Eighth Annual IEEE Symp. on Logic in Computer Science, {LICS} 1993}, year = 1993, editor = {Moshe Vardi}, month = {June}, pages = {39--46}, location = {Montreal, Canada}, publisher = {IEEE Computer Society Press} }