{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:59:42Z","timestamp":1773097182276,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":16,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540578871","type":"print"},{"value":"9783540483830","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1994]]},"DOI":"10.1007\/3-540-57887-0_112","type":"book-chapter","created":{"date-parts":[[2012,2,26]],"date-time":"2012-02-26T13:38:26Z","timestamp":1330263506000},"page":"495-515","source":"Crossref","is-referenced-by-count":18,"title":["A symmetric lambda calculus for \u201cclassical\u201d program extraction"],"prefix":"10.1007","author":[{"given":"Franco","family":"Barbanera","sequence":"first","affiliation":[]},{"given":"Stefano","family":"Berardi","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2005,5,31]]},"reference":[{"key":"26_CR1","unstructured":"F. Barbanera, S. Berardi, \u201dWitness Extraction in Classical Logic through Normalization\u201d, in Logical Environments, edited by G.Huet and G.Plotkin, Cambridge University Press, 1993."},{"key":"26_CR2","doi-asserted-by":"crossref","unstructured":"F. Barbanera, S. Berardi, \u201dA constructive valuation interpretation for classical logic and its use in witness extraction\u201d, Proceedings of Colloquium on Trees in Algebra and Programming (CAAP), LNCS 581, Springer Verlag, 1992.","DOI":"10.1007\/3-540-55251-0_1"},{"key":"26_CR3","unstructured":"F. Barbanera, S. Berardi, \u201dExtracting constructive content from classical proofs via control like reductions\u201d, Proceedings of the International conference on Typed Lambda Calculus and applications (TLCA) 93, LNCS, Springer Verlag, 1993."},{"key":"26_CR4","unstructured":"R.L. Constable, S. Allen, H. Bromely, W. Cleaveland et al., Implementing Mathematics with the Nuprl Proof Development System, Prentice-Hall, 1986."},{"key":"26_CR5","unstructured":"T. Coquand, \u201cA Game-theoric semantic of Classical Logic\u201d, 1992, submitted for publication."},{"key":"26_CR6","doi-asserted-by":"crossref","unstructured":"H. Friedman, \u201cClassically and intuitionistically provably recursive functions\u201d, in Higher Set Theory, eds. Scott D.S. and Muller G.H., Lecture Notes in Mathematics vol.699, 21\u201328, Springer Verlag, 1978.","DOI":"10.1007\/BFb0103100"},{"key":"26_CR7","unstructured":"J.-Y. Girard, Interpr\u00e9tation fonctionelle et \u00e9limination des coupures dans l'arithm\u00e9tique d'ordre superi\u00e9ur, Th\u00e9se de Doctorat d'Etat, University of Paris, 1972."},{"key":"26_CR8","doi-asserted-by":"crossref","unstructured":"T.G. Griffin, \u201cA formulae-as-types notion of control\u201d, in Proceedings of the Seventeenth Annual ACM Symposium on Principles of Programming languages, 1990.","DOI":"10.1145\/96709.96714"},{"key":"26_CR9","doi-asserted-by":"crossref","first-page":"155","DOI":"10.2307\/2964396","volume":"23","author":"G. Kreisel","year":"1958","unstructured":"G. Kreisel, \u201cMathematical significance of consistency proofs\u201d, Journal of Symbolic Logic, 23:155\u2013182, 1958.","journal-title":"Journal of Symbolic Logic"},{"key":"26_CR10","unstructured":"C. Murthy, Extracting constructive content from classical proofs, Ph.D. thesis, 90\u20131151, department of Computer Science, Cornell University, 1990."},{"key":"26_CR11","unstructured":"B. Nordstr\u00f6m, K. Petersson and J. Smith, Programming in Martin-L\u00f6f's Type Theory, OUP, 1990."},{"key":"26_CR12","doi-asserted-by":"crossref","first-page":"190","DOI":"10.1007\/BFb0013061","volume":"624","author":"M. Parigot","year":"1992","unstructured":"M. Parigot, \u03bb\u03bc-calculus: an algorithmic interpretation of classical natural deduction, Proceedings LPAR'92, Lecture Notes in Computer Science vol. 624, 190\u2013201, 1992.","journal-title":"Proceedings LPAR'92, Lecture Notes in Computer Science"},{"key":"26_CR13","unstructured":"L.C. Paulson and T. Nipkow, \u201cIsabelle tutorial and user's manual\u201d, technical report 189, University of Cambridge, 1990."},{"key":"26_CR14","volume-title":"Natural deduction, a proof theoretical study","author":"D. Prawitz","year":"1965","unstructured":"D. Prawitz, Natural deduction, a proof theoretical study, Stockolm, Almqvist and Winskell, 1965."},{"key":"26_CR15","first-page":"11","volume-title":"Atti del I Congresso Italiano di Logica","author":"D. Prawitz","year":"1981","unstructured":"D. Prawitz, \u201cValidity and normalizability of proofs in 1-st and 2-nd order classical and intuitionistic logic\u201d, in Atti del I Congresso Italiano di Logica, Napoli, Bibliopolis, 11\u201336, 1981."},{"key":"26_CR16","doi-asserted-by":"crossref","unstructured":"W.W. Tait, \u201cIntensional interpretation of functional of finite types\u201d, journal of Symbolic Logic 32, 1967.","DOI":"10.2307\/2271658"}],"container-title":["Lecture Notes in Computer Science","Theoretical Aspects of Computer Software"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/3-540-57887-0_112.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,11,17]],"date-time":"2020-11-17T21:15:28Z","timestamp":1605647728000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/3-540-57887-0_112"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1994]]},"ISBN":["9783540578871","9783540483830"],"references-count":16,"URL":"https:\/\/doi.org\/10.1007\/3-540-57887-0_112","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1994]]}}}