DocumentCode
1823155
Title
Strong normalization for second order classical natural deduction
Author
Parigot, Michel
Author_Institution
Paris VII Univ., France
fYear
1993
fDate
19-23 Jun 1993
Firstpage
39
Lastpage
46
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
Keywords
inference mechanisms; lambda calculus; reducibility candidates; second order classical natural deduction; second-order intuitionistic natural deduction; strong normalization theorem; Calculus; Filters; H infinity control; Logic programming;
fLanguage
English
Publisher
ieee
Conference_Titel
Logic in Computer Science, 1993. LICS '93., Proceedings of Eighth Annual IEEE Symposium on
Conference_Location
Montreal, Que.
Print_ISBN
0-8186-3140-6
Type
conf
DOI
10.1109/LICS.1993.287602
Filename
287602
Link To Document