Lics

IEEE Symposium on Logic in Computer Science

Paper: Strong normalization for second order classical natural deduction (at LICS 1993)

Abstract

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 Symposium on Logic in Computer Science (LICS 1993)},
 year =	 {1993},
 month =	 {June}, 
 pages = {39--46},
 location = {Montreal, Canada}, 
 publisher =	 {IEEE Computer Society Press}
 }