{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,24]],"date-time":"2025-03-24T06:54:20Z","timestamp":1742799260091},"reference-count":18,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2007,7,6]],"date-time":"2007-07-06T00:00:00Z","timestamp":1183680000000},"content-version":"tdm","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Theory Comput Syst"],"published-print":{"date-parts":[[2008,12]]},"DOI":"10.1007\/s00224-007-9027-4","type":"journal-article","created":{"date-parts":[[2007,7,5]],"date-time":"2007-07-05T13:30:13Z","timestamp":1183642213000},"page":"583-602","source":"Crossref","is-referenced-by-count":7,"title":["Realizability interpretation of proofs in constructive analysis"],"prefix":"10.1007","volume":"43","author":[{"given":"Helmut","family":"Schwichtenberg","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,7,6]]},"reference":[{"key":"9027_CR1","unstructured":"Andersson, P.: Exact real arithmetic with automatic error estimates in a computer algebra system. Master\u2019s thesis, Mathematics Department, Uppsala University (2001)"},{"issue":"2","key":"9027_CR2","doi-asserted-by":"crossref","first-page":"201","DOI":"10.1002\/malq.200410020","volume":"51","author":"J. Berger","year":"2005","unstructured":"Berger, J.: Exact calculation of inverse functions. Math. Log. Q. 51(2), 201\u2013205 (2005)","journal-title":"Math. Log. Q."},{"key":"9027_CR3","doi-asserted-by":"crossref","first-page":"125","DOI":"10.1016\/j.apal.2004.10.006","volume":"133","author":"U. Berger","year":"2005","unstructured":"Berger, U.: Uniform Heyting arithmetic. Ann. Pure Appl. Log. 133, 125\u2013148 (2005)","journal-title":"Ann. Pure Appl. Log."},{"key":"9027_CR4","series-title":"Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"91","DOI":"10.1007\/BFb0037100","volume-title":"Typed Lambda Calculi and Applications","author":"U. Berger","year":"1993","unstructured":"Berger, U.: Program extraction from normalization proofs. In: Bezem, M., Groote, J. (eds.) Typed Lambda Calculi and Applications. Lecture Notes in Comput. Sci., vol. 664, pp. 91\u2013106. Springer, Berlin (1993)"},{"key":"9027_CR5","doi-asserted-by":"crossref","first-page":"19","DOI":"10.1016\/S0890-5401(03)00014-2","volume":"183","author":"U. Berger","year":"2003","unstructured":"Berger, U., Eberl, M., Schwichtenberg, H.: Term rewriting for normalization by evaluation. Inf. Comput. 183, 19\u201342 (2003)","journal-title":"Inf. Comput."},{"key":"9027_CR6","volume-title":"Foundations of Constructive Analysis","author":"E. Bishop","year":"1967","unstructured":"Bishop, E.: Foundations of Constructive Analysis. McGraw-Hill, New York (1967)"},{"key":"9027_CR7","unstructured":"Cruz-Filipe, L.: Constructive real analysis: a type-theoretical formalization and applications. Ph.D. Thesis, Nijmegen University (2004)"},{"key":"9027_CR8","series-title":"Lecture Notes in Comput. Sci.","first-page":"96","volume-title":"Proc. Types 2000","author":"H. Geuvers","year":"2000","unstructured":"Geuvers, H., Wiedijk, F., Zwanenburg, J.: A constructive proof of the fundamental theorem of algebra without using the rationals. In: Callaghan, P., Luo, Z., McKinna, J., Pollack, R. (eds.) Proc. Types 2000. Lecture Notes in Comput. Sci., vol. 2277, pp. 96\u2013111. Springer, Berlin (2000)"},{"key":"9027_CR9","doi-asserted-by":"crossref","first-page":"280","DOI":"10.1111\/j.1746-8361.1958.tb01464.x","volume":"12","author":"K. G\u00f6del","year":"1958","unstructured":"G\u00f6del, K.: \u00dcber eine bisher noch nicht ben\u00fctzte Erweiterung des finiten Standpunkts. Dialectica 12, 280\u2013287 (1958)","journal-title":"Dialectica"},{"key":"9027_CR10","volume-title":"Lectures on Ordinary Differential Equations","author":"W. Hurewicz","year":"1958","unstructured":"Hurewicz, W.: Lectures on Ordinary Differential Equations. MIT Press, Cambridge (1958)"},{"key":"9027_CR11","unstructured":"Kohlenbach, U.: Real growth in standard parts of analysis. Habilitationsschrift, Fachbereich Mathematik, Universit\u00e4t Frankfurt am Main (1995)"},{"key":"9027_CR12","doi-asserted-by":"crossref","unstructured":"Kohlenbach, U.: Proof theory and computational analysis. Electron. Notes Theor. Comput. Sci. 13 (1998), 34 p.","DOI":"10.1016\/S1571-0661(05)80219-1"},{"key":"9027_CR13","first-page":"101","volume-title":"Constructivity in Mathematics","author":"G. Kreisel","year":"1959","unstructured":"Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. In: Heyting, A. (ed.) Constructivity in Mathematics, pp. 101\u2013128. North-Holland, Amsterdam (1959)"},{"key":"9027_CR14","series-title":"Lecture Notes in Comput. Sci.","volume-title":"Types for Proofs and Programs, Second International Workshop, TYPES 2002","author":"P. Letouzey","year":"2003","unstructured":"Letouzey, P.: A new extraction for Coq. In: Geuvers, H., Wiedijk, F. (eds.) Types for Proofs and Programs, Second International Workshop, TYPES 2002. Lecture Notes in Comput. Sci., vol. 2646. Springer, Berlin (2003)"},{"issue":"2","key":"9027_CR15","doi-asserted-by":"crossref","first-page":"413","DOI":"10.2140\/pjm.1982.99.413","volume":"99","author":"M. Mandelkern","year":"1982","unstructured":"Mandelkern, M.: Continuity of monotone functions. Pac. J. Math. 99(2), 413\u2013418 (1982)","journal-title":"Pac. J. Math."},{"key":"9027_CR16","volume-title":"Interval Analysis","author":"R.E. Moore","year":"1966","unstructured":"Moore, R.E.: Interval Analysis. Prentice-Hall, Englewood Cliffs (1966)"},{"key":"9027_CR17","series-title":"Series III: Computer and Systems Sciences","first-page":"323","volume-title":"Proof Technology and Computation. Proc. NATO Advanced Study Institute, Marktoberdorf, 2003","author":"H. Schwichtenberg","year":"2006","unstructured":"Schwichtenberg, H.: Constructive analysis with witnesses. In: Schwichtenberg, H., Spies, K. (eds.) Proof Technology and Computation. Proc. NATO Advanced Study Institute, Marktoberdorf, 2003. Series III: Computer and Systems Sciences, vol. 200, pp. 323\u2013353. IOS Press, Utrecht (2006)"},{"key":"9027_CR18","series-title":"Lecture Notes in Math.","volume-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","year":"1973","unstructured":"Troelstra, A.S. (ed.): Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Math., vol. 344. Springer, Berlin (1973)"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9027-4.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-007-9027-4\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9027-4","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,24]],"date-time":"2019-05-24T07:51:34Z","timestamp":1558684294000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-007-9027-4"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7,6]]},"references-count":18,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["9027"],"URL":"https:\/\/doi.org\/10.1007\/s00224-007-9027-4","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,7,6]]}}}