Abstract
Recently there has been much interest in the problem of finding the computational content of classical reasoning. One of the most appealing directions for the computer scientist to tackle such a problem is the relation which has been established between classical logic and lambda calculi with control operators, like Felleisen's control operator C. In this paper we introduce a typed lambda calculus with the C operator corresponding to Peano Arithmetic, and a set of reduction rules related to the ones of the usual control calculi with C. We show how these rules, which are proved to be strongly normalizing, can be used to extract witnesses from proofs of ∑ 01 sentences in Peano Arithmetic.
To Roberta Gottardi
This is a preview of subscription content, log in via an institution to check access.
Preview
Unable to display preview. Download preview PDF.
References
Barbanera F., Berardi S. A constructive valuation interpretation for classical logic and its use in witness extraction. Proceedings of Colloquium on Trees in Algebra and Programming (CAAP), LNCS 581, Springer Verlag, 1992.
Barbanera F., Berardi S. Continuations and simple types: a strong normalization result. Proceedings of the ACM SIGPLAN Workshop on Continuations. Report No STAN-CS-92-1426 Stanford University. San Francisco, June 1992.
Coquand T. A Game-theoric semantic of Classical Logic, 1992, submitted to JSL
M. Felleisen, R. Ilieb, The revised report on the syntactic theories of sequential control. Technical report 100, University of Rice, Houston, 1989. To appear in Theoretical Computer Science.
M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba, Reasoning with continuations. In ”Proceedings of the First Annual Symposium on Logic in Computer Science”, pages 131–141,1986.
Friedman H. Classically and intuitionistically provably recursive functions. In Scott D.S. and Muller G.H. editors, Higher Set Theory, vol.699 of Lecture Notes in Mathematics, 21–28. Springer Verlag, 1978.
Girard Y.J. A new constructive logic: Classical Logic, in MSCS, n. 1, 1990.
Timothy G. Griffin. A formulas-as-types notion of control. In ”Conference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages”, 1990.
Kreisel G. Mathematical significance of consistency proofs. Journal of Symbolic Logic, 23:155–182, 1958.
Murthy C. Extracting constructive content from classical proofs. Ph.d. thesis, Department of Computer science, Cornell University, 1990.
Parigot M. lambda-mu-calculus: an algorithmic interpretation of classical natural deduction. Manuscript.
Prawitz D. Validity and normalizability of proofs in 1-st and 2-nd order classical and intuitionistic logic. In Atti del I Congresso Italiano di Logica, Napoli, Bibliopolis, 11–36, 1981.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1993 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Barbanera, F., Berardi, S. (1993). Extracting constructive content from classical logic via control-like reductions. In: Bezem, M., Groote, J.F. (eds) Typed Lambda Calculi and Applications. TLCA 1993. Lecture Notes in Computer Science, vol 664. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0037097
Download citation
DOI: https://doi.org/10.1007/BFb0037097
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-56517-8
Online ISBN: 978-3-540-47586-6
eBook Packages: Springer Book Archive