{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,3,9]],"date-time":"2026-03-09T22:58:31Z","timestamp":1773097111293,"version":"3.50.1"},"publisher-location":"Berlin, Heidelberg","reference-count":19,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"value":"9783540590484","type":"print"},{"value":"9783540491781","type":"electronic"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[1995]]},"DOI":"10.1007\/bfb0014044","type":"book-chapter","created":{"date-parts":[[2005,11,23]],"date-time":"2005-11-23T07:50:31Z","timestamp":1132732231000},"page":"47-62","source":"Crossref","is-referenced-by-count":2,"title":["A realization of the negative interpretation of the Axiom of Choice"],"prefix":"10.1007","author":[{"given":"Stefano","family":"Berardi","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Marc","family":"Bezem","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Thierry","family":"Coquand","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2005,6,9]]},"reference":[{"key":"4_CR1","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1007\/BF01449946","volume":"93","author":"W. Ackermann","year":"1924","unstructured":"W. Ackermann. Begr\u00fcndung des Tertium non datur mittels der Hilbertschen Theorie der Widerspruchsfreiheit. Mathematische Annalen, 93, 1924, p. 1\u201336","journal-title":"Mathematische Annalen"},{"key":"4_CR2","doi-asserted-by":"publisher","first-page":"175","DOI":"10.1007\/BF02007566","volume":"25","author":"M. Bezem","year":"1985","unstructured":"M. Bezem. Strong Normalization of Barrecursive Terms Without Using Infinite Terms. Archiv f\u00fcr mathematische Logik und Grundlagenforschung, 25, 1985, p. 175\u2013182","journal-title":"Archiv f\u00fcr mathematische Logik und Grundlagenforschung"},{"key":"4_CR3","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"E. Bishop. Foundations of Constructive Analysis. New York, McGraw-Hill, 1967."},{"key":"4_CR4","doi-asserted-by":"crossref","unstructured":"R. Constable and C. Murthy. Finding Computational Content in Classical Proofs. In G. Huet and G. Plotkin, editors, Logical Frameworks, 341\u2013362, (1991), Cambridge University Press.","DOI":"10.1017\/CBO9780511569807.014"},{"key":"4_CR5","unstructured":"Th. Coquand. A semantics of evidence for classical arithmetic. Journal of Symbolic Logic, to appear, 1994."},{"key":"4_CR6","unstructured":"K. G\u00f6del. Collected Work. Volumes I and II, S. Feferman, J. W. Dawson, S.C. Kleene, G.H. Moore, R. M. Solovay, J. van Heijenoort, editors, Oxford, 1986."},{"key":"4_CR7","unstructured":"N. Goodman. Intuitionistic arithmetic as a theory of constructions. PhD thesis, Stanford University, 1968."},{"key":"4_CR8","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1007\/BF01448445","volume":"88","author":"D. Hilbert","year":"1923","unstructured":"D. Hilbert. Die logischen Grundlagen der Mathematik. Mathematische Annalen, 88, 1923, p. 151\u2013165","journal-title":"Mathematische Annalen"},{"key":"4_CR9","unstructured":"D. Hilbert. The foundations of mathematics. In van Heijenoort ed., From Frege to G\u00f6del, p. 465\u2013479."},{"key":"4_CR10","first-page":"107","volume":"20","author":"W.A. Howard","year":"1968","unstructured":"W.A. Howard. Functional interpretation of bar induction by bar recursion. Compos. Mathematica 20 (1968), 107\u2013124.","journal-title":"Compos. Mathematica"},{"key":"4_CR11","first-page":"414","volume-title":"From Frege to G\u00f6del","author":"A.N. Kolmogorov","year":"1971","unstructured":"A.N. Kolmogorov. On the principle of the excluded middle. In From Frege to G\u00f6del, J. van Heijenoort, editor, Harvard University Press, Cambridge MA, 1971, pp. 414\u2013437."},{"key":"4_CR12","first-page":"95","volume-title":"Lectures on Modern Mathematics, vol. III","author":"G. Kreisel","year":"1965","unstructured":"G. Kreisel. Mathematical Logic. In Lectures on Modern Mathematics, vol. III, ed. Saaty, Wiley, N.Y., 1965, p. 95\u2013195."},{"key":"4_CR13","doi-asserted-by":"crossref","unstructured":"G.E. Moore. Zermelo's Axiom of Choice: Its Origins, Development and Influence. Springer-Verlag, 1982","DOI":"10.1007\/978-1-4613-9478-5"},{"key":"4_CR14","unstructured":"C. Murthy. Extracting Constructive Content from Classical Proofs. Ph. D. Thesis, 1990."},{"key":"4_CR15","doi-asserted-by":"crossref","unstructured":"C. Spector. Provably recursive functionals of analysis: a consistency proof of analysis by an extension of principles formulated in current intuitionistic mathematics. Recursive Function Theory, J.C.E. Dekker ed., Proceedings of Symposia in Pure Mathematics V, AMS, p. 1\u201327, 1961.","DOI":"10.1090\/pspum\/005\/0154801"},{"key":"4_CR16","doi-asserted-by":"crossref","unstructured":"D.N. Osherbon, M. Stob and S. Weinstein. Systems That Learn: An Introduction to Learning Theory for Cognitive and Computer Scientists. MIT Press, 1986.","DOI":"10.7551\/mitpress\/6609.001.0001"},{"key":"4_CR17","first-page":"353","volume-title":"Normal form theorem for bar recursive functions of finite type","author":"W.W. Tait","year":"1971","unstructured":"W.W. Tait. Normal form theorem for bar recursive functions of finite type. In Proceedings of the second Scandinavian Logic Symposium, J.E. Fenstad ed., North Holland, Amsterdam, 1971, pp. 353\u2013367."},{"key":"4_CR18","volume-title":"Lecture Notes in Mathematics 344","author":"A.S. Troelstra","year":"1973","unstructured":"A.S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics 344, Springer-Verlag, Berlin, 1973."},{"key":"4_CR19","unstructured":"A.S. Troelstra. Realizability. ILLC Prepublication Series for Mathematical Logic and Foundations ML-92-09."}],"container-title":["Lecture Notes in Computer Science","Typed Lambda Calculi and Applications"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/BFb0014044","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,11]],"date-time":"2020-04-11T04:37:49Z","timestamp":1586579869000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/BFb0014044"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1995]]},"ISBN":["9783540590484","9783540491781"],"references-count":19,"URL":"https:\/\/doi.org\/10.1007\/bfb0014044","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"value":"0302-9743","type":"print"},{"value":"1611-3349","type":"electronic"}],"subject":[],"published":{"date-parts":[[1995]]}}}