Logic in Computer Science (LICS 1993)

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

Authors: Michel Parigot

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 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}
  }