• 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