{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:50:39Z","timestamp":1773096639686,"version":"3.50.1"},"publisher-location":"Berlin\/Heidelberg","reference-count":12,"publisher":"Springer-Verlag","isbn-type":[{"value":"3540565175","type":"print"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"DOI":"10.1007\/bfb0037097","type":"book-chapter","created":{"date-parts":[[2006,1,25]],"date-time":"2006-01-25T15:21:36Z","timestamp":1138202496000},"page":"45-59","source":"Crossref","is-referenced-by-count":19,"title":["Extracting constructive content from classical logic via control-like reductions"],"prefix":"10.1007","author":[{"given":"Franco","family":"Barbanera","sequence":"first","affiliation":[]},{"given":"Stefano","family":"Berardi","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"4_CR1","doi-asserted-by":"crossref","unstructured":"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.","DOI":"10.1007\/3-540-55251-0_1"},{"key":"4_CR2","volume-title":"Report No STAN-CS-92-1426","author":"F. Barbanera","year":"1992","unstructured":"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."},{"key":"4_CR3","unstructured":"Coquand T. A Game-theoric semantic of Classical Logic, 1992, submitted to JSL"},{"key":"4_CR4","volume-title":"Technical report 100","author":"M. Felleisen","year":"1989","unstructured":"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."},{"key":"4_CR5","unstructured":"M. Felleisen, D. Friedman, E. Kohlbecker, and B. Duba, Reasoning with continuations. In \u201dProceedings of the First Annual Symposium on Logic in Computer Science\u201d, pages 131\u2013141,1986."},{"key":"4_CR6","doi-asserted-by":"crossref","unstructured":"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\u201328. Springer Verlag, 1978.","DOI":"10.1007\/BFb0103100"},{"key":"4_CR7","doi-asserted-by":"crossref","unstructured":"Girard Y.J. A new constructive logic: Classical Logic, in MSCS, n. 1, 1990.","DOI":"10.1017\/S0960129500001328"},{"key":"4_CR8","doi-asserted-by":"crossref","unstructured":"Timothy G. Griffin. A formulas-as-types notion of control. In \u201dConference Record of the Seventeenth Annual ACM Symposium on Principles of Programming Languages\u201d, 1990.","DOI":"10.1145\/96709.96714"},{"key":"4_CR9","doi-asserted-by":"crossref","first-page":"155","DOI":"10.2307\/2964396","volume":"23","author":"G. Kreisel","year":"1958","unstructured":"Kreisel G. Mathematical significance of consistency proofs. Journal of Symbolic Logic, 23:155\u2013182, 1958.","journal-title":"Journal of Symbolic Logic"},{"key":"4_CR10","unstructured":"Murthy C. Extracting constructive content from classical proofs. Ph.d. thesis, Department of Computer science, Cornell University, 1990."},{"key":"4_CR11","unstructured":"Parigot M. lambda-mu-calculus: an algorithmic interpretation of classical natural deduction. Manuscript."},{"key":"4_CR12","first-page":"11","volume-title":"Atti del I Congresso Italiano di Logica","author":"D. Prawitz","year":"1981","unstructured":"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\u201336, 1981."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0037097.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,12,9]],"date-time":"2020-12-09T22:22:00Z","timestamp":1607552520000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0037097"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[null]]},"ISBN":["3540565175"],"references-count":12,"URL":"https:\/\/doi.org\/10.1007\/bfb0037097","relation":{},"subject":[]}}