Hostname: page-component-745bb68f8f-f46jp Total loading time: 0 Render date: 2025-01-07T20:00:37.519Z Has data issue: false hasContentIssue false
  • English
  • Français

Proofs of strong normalisation for second order classical natural deduction

Published online by Cambridge University Press:  12 March 2014

Michel Parigot
Michel Parigot*
Affiliation:
Equipe de Logique—CNRS UA 753, 45-55 5Ème Étage, Université Paris7, 2 Place Jussieu, 75251 Paris Cedex 05, France E-mail: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

We give two proofs of strong normalisation for second order classical natural deduction. The first one is an adaptation of the method of reducibility candidates introduced in [9] for second order intuitionistic natural deduction; the extension to the classical case requires in particular a simplification of the notion of reducibility candidate. The second one is a reduction to the intuitionistic case, using a Kolmogorov translation.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 62 , Issue 4 , December 1997 , pp. 1461 - 1479
Copyright
Copyright © Association for Symbolic Logic 1997

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Barendregt, H., The lambda-calculus, North-Holland, 1981.Google Scholar
[2]Berardi, S. and Barbanera, F., A symmetric lambda-calculus for “classical” program extraction, draft, 1994.CrossRefGoogle Scholar
[3]Coquand, T., A semantics of evidence for classical arithmetic, this Journal, vol. 60 (1995), pp. 325–337.Google Scholar
[4]Danos, V., Une application de la logique linéaire à l'étude des processus de normalisation, Ph.D. thesis, Université Paris 7, 1990.Google Scholar
[5]Danos, V., Joinet, J. B., and Schellinx, H., A new deconstructive logic: linear logic, to appear in this Journal.Google Scholar
[6]DeGroote, P., A CPS-translation of the λü-calculus, Proceedings of CAAP '94, Lecture Notes in Computer Science, no. 787, Springer-Verlag, 1994, pp. 85–99.Google Scholar
[7]Fortune, S., Leivant, D., and O'Donnell, M., The expressiveness of simple and second order type structures, Journal of the Association for Computing Machinery, vol. 30 (1983), pp. 151–185.CrossRefGoogle Scholar
[8]Gallier, J. H., On Girard's “candidats de réductibilités”, Logic and computer science (Odifreddi, P., editor), Academic Press, 1990, pp. 123–203.Google Scholar
[9]Girard, J. Y., Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieure, Ph.D. thesis, Université Paris 7, 1972.Google Scholar
[10]Girard, J. Y., Linear logic, Theoretical Computer Science, vol. 50 (1987), pp. 1–102.CrossRefGoogle Scholar
[11]Girard, J. Y., A new constructive logic: classical logic, Mathematical Structures in Computer Science, vol. 1 (1991), pp. 255–296.CrossRefGoogle Scholar
[12]Girard, J. Y., Lafont, Y., and Taylor, P., Proofs and types, Cambridge University Press, 1989.Google Scholar
[13]Griffin, T., A formulae-as-types notion of control, Proceedings of POPL, 1990, pp. 47–58.Google Scholar
[14]Krivine, J. L., Lambda-calcul, types et modèles, Masson, 1990.Google Scholar
[15]Murthy, C., Extracting constructive content from classical proofs, Ph.D. thesis, Cornell, 1990.Google Scholar
[16]Parigot, M., Internal labellings in lambda-calculus, Proceedings of MFCS (Bystrica, Banská, editor), Lecture Notes in Computer Science, no. 452, 1990, pp. 439–445.Google Scholar
[17]Parigot, M., Free deduction: an analysis of “computations” in classical logic, Proceedings of the Russian conference on logic programming, Lecture Notes in Computer Science, no. 592, Springer-Verlag, 1991, pp. 361–380.Google Scholar
[18]Parigot, M., λü-calculus: an algorithmic interpretation of classical natural deduction, Proceedings of the international conference on logic programming and automated reasoning, Lecture Notes in Computer Science, no. 624, Springer-Verlag, 1992, pp. 190–201.CrossRefGoogle Scholar
[19]Plotkin, G., Call-by-name, call-by-value and the λ-calculus, Theoretical Computer Science, vol. 1 (1975), pp. 125–159.CrossRefGoogle Scholar
[20]Rezus, A., Beyond BHK, draft, 1993.Google Scholar