{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:33:23Z","timestamp":1759638803161},"reference-count":23,"publisher":"Springer Science and Business Media LLC","issue":"3","license":[{"start":{"date-parts":[[2011,4,14]],"date-time":"2011-04-14T00:00:00Z","timestamp":1302739200000},"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":[[2012,10]]},"DOI":"10.1007\/s00224-011-9325-8","type":"journal-article","created":{"date-parts":[[2011,4,13]],"date-time":"2011-04-13T02:17:34Z","timestamp":1302661054000},"page":"313-329","source":"Crossref","is-referenced-by-count":12,"title":["Proofs, Programs, Processes"],"prefix":"10.1007","volume":"51","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[]},{"given":"Monika","family":"Seisenberger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2011,4,14]]},"reference":[{"key":"9325_CR1","series-title":"Applied Logic Series","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/978-94-017-0435-9_2","volume-title":"Automated Deduction\u2014A Basis for Applications","author":"H. Benl","year":"1998","unstructured":"Benl, H., Berger, U., Schwichtenberg, H., Seisenberger, M., Zuber, W.: Proof theory at work: Program development in the Minlog system. In: Bibel, W., Schmitt, P.H. (eds.) Automated Deduction\u2014A Basis for Applications. Applied Logic Series, vol. II, pp. 41\u201371. Kluwer, Dordrecht (1998)"},{"key":"9325_CR2","doi-asserted-by":"crossref","unstructured":"Berger, U.: From coinductive proofs to exact real arithmetic: theory and applications. Log. Methods Comput. Sci. 7(1), (2011)","DOI":"10.2168\/LMCS-7(1:8)2011"},{"key":"9325_CR3","doi-asserted-by":"crossref","first-page":"37","DOI":"10.1017\/S0960129506005809","volume":"17","author":"Y. Bertot","year":"2007","unstructured":"Bertot, Y.: Affine functions and series with co-inductive real numbers. Math. Struct. Comput. Sci. 17, 37\u201363 (2007)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9325_CR4","series-title":"Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"132","DOI":"10.1007\/978-3-642-04027-6_12","volume-title":"Computer Science Logic","author":"U. Berger","year":"2009","unstructured":"Berger, U.: From coinductive proofs to exact real arithmetic. In: Gr\u00e4del, E., Kahle, R. (eds.) Computer Science Logic. Lecture Notes in Comput. Sci., vol. 5771 pp. 132\u2013146. Springer, Berlin (2009)"},{"issue":"18","key":"9325_CR5","first-page":"2535","volume":"16","author":"U. Berger","year":"2010","unstructured":"Berger, U.: Realisability for induction and coinduction with applications to constructive analysis. J. Univers. Comput. Sci. 16(18), 2535\u20132555 (2010)","journal-title":"J. Univers. Comput. Sci."},{"key":"9325_CR6","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0091894","volume-title":"Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof\u2013Theoretical Studies","author":"W. Buchholz","year":"1981","unstructured":"Buchholz, W., Feferman, F., Pohlers, W., Sieg, W.: Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof\u2013Theoretical Studies. Lecture Notes in Mathematics, vol.\u00a0897. Springer, Berlin (1981)"},{"key":"9325_CR7","doi-asserted-by":"crossref","first-page":"394","DOI":"10.1007\/s00224-007-9017-6","volume":"43","author":"U. Berger","year":"2008","unstructured":"Berger, U., Hou, T.: Coinduction for exact real number computation. Theory Comput. Syst. 43, 394\u2013409 (2008)","journal-title":"Theory Comput. Syst."},{"key":"9325_CR8","series-title":"Proceedings of Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1007\/978-3-642-13962-8_5","volume-title":"Programs, Proofs, Processes, 6th Conference on Computability in Europe, CiE 2010","author":"U. Berger","year":"2010","unstructured":"Berger, U., Seisenberger, M.: Proofs, programs, processes. In: Ferreira, F., L\u00f6we, B., Mayordomo, E., Gomes, L.M. (eds.) Programs, Proofs, Processes, 6th Conference on Computability in Europe, CiE 2010, Ponta Delgada, Azores, Portugal, June 30\u2013July 4, 2010. Proceedings of Lecture Notes in Comput. Sci., vol. 6158, pp. 39\u201348. (2010)"},{"key":"9325_CR9","doi-asserted-by":"crossref","first-page":"39","DOI":"10.1016\/j.tcs.2005.09.061","volume":"351","author":"A. Ciaffaglione","year":"2006","unstructured":"Ciaffaglione, A., Di Gianantonio, P.: A certified, corecursive implementation of exact real numbers. Theor. Comput. Sci. 351, 39\u201351 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"9325_CR10","unstructured":"The Coq Proof Assistant. http:\/\/coq.inria.fr\/"},{"key":"9325_CR11","first-page":"193","volume-title":"Applied Semantics\u2014Lecture Notes from the International Summer School, Caminha, Portugal","author":"A. Edalat","year":"2002","unstructured":"Edalat, A., Heckmann, R.: Computing with real numbers: I. The LFT approach to real number computation; II. A domain framework for computational geometry. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) Applied Semantics\u2014Lecture Notes from the International Summer School, Caminha, Portugal, pp. 193\u2013267. Springer, Berlin (2002)"},{"key":"9325_CR12","doi-asserted-by":"crossref","first-page":"141","DOI":"10.1016\/j.entcs.2006.06.009","volume":"164","author":"N. Ghani","year":"2006","unstructured":"Ghani, N., Hancock, P., Pattinson, D.: Continuous functions on final coalgebras. Electron. Notes Theor. Comput. Sci. 164, 141\u2013155 (2006)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1","key":"9325_CR13","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1017\/S0960129506005834","volume":"17","author":"H. Geuvers","year":"2007","unstructured":"Geuvers, H., Niqui, M., Spitters, B., Wiedijk, F.: Constructive analysis, types and exact real numbers. Math. Struct. Comput. Sci. 17(1), 3\u201336 (2007)","journal-title":"Math. Struct. Comput. Sci."},{"key":"9325_CR14","series-title":"Lecture Notes in Comput. Sci.","doi-asserted-by":"crossref","first-page":"251","DOI":"10.1007\/978-3-540-69407-6_29","volume-title":"CiE 2008: Logic and Theory of Algorithms","author":"M.D. Hernest","year":"2008","unstructured":"Hernest, M.D., Oliva, P.: Hybrid functional interpretations. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008: Logic and Theory of Algorithms. Lecture Notes in Comput. Sci., vol. 5028, pp. 251\u2013260. Springer, Berlin (2008)"},{"key":"9325_CR15","doi-asserted-by":"crossref","first-page":"259","DOI":"10.1016\/S0304-3975(02)00776-4","volume":"308","author":"J.-L. Krivine","year":"2003","unstructured":"Krivine, J.-L.: Dependent choice, \u2018quote\u2019 and the clock. Theor. Comput. Sci. 308, 259\u2013276 (2003)","journal-title":"Theor. Comput. Sci."},{"key":"9325_CR16","unstructured":"The Minlog System. http:\/\/www.mathematik.uni-muenchen.de\/~minlog\/"},{"key":"9325_CR17","doi-asserted-by":"crossref","first-page":"179","DOI":"10.1016\/j.entcs.2004.04.048","volume":"123","author":"F. Miranda-Perea","year":"2005","unstructured":"Miranda-Perea, F.: Realizability for monotone clausular (co)inductive definitions. Electron. Notes Theor. Comput. Sci. 123, 179\u2013193 (2005)","journal-title":"Electron. Notes Theor. Comput. Sci."},{"issue":"1\u20132","key":"9325_CR18","doi-asserted-by":"crossref","first-page":"120","DOI":"10.1016\/j.tcs.2007.01.021","volume":"379","author":"J.R. Marcial-Romero","year":"2007","unstructured":"Marcial-Romero, J.R., Escardo, M.H.: Semantics of a sequential language for exact real-number computation. Theor. Comput. Sci. 379(1\u20132), 120\u2013141 (2007)","journal-title":"Theor. Comput. Sci."},{"issue":"3\u20136","key":"9325_CR19","first-page":"1","volume":"4","author":"M. Niqui","year":"2008","unstructured":"Niqui, M.: Coinductive formal reasoning in exact real arithmetic. Log. Methods Comput. Sci. 4(3\u20136), 1\u201340 (2008)","journal-title":"Log. Methods Comput. Sci."},{"key":"9325_CR20","unstructured":"Plume, D.: A calculator for exact real number computation. Master\u2019s thesis, University of Edinburgh, 1998"},{"key":"9325_CR21","doi-asserted-by":"crossref","unstructured":"Ratiu, D., Trifonov, T.: Exploring the computational content of the infinite pigeonhole principle. J.\u00a0Logic Comput. doi: 10.1093\/logcom\/exq011","DOI":"10.1093\/logcom\/exq011"},{"issue":"3\u20134","key":"9325_CR22","doi-asserted-by":"crossref","first-page":"583","DOI":"10.1007\/s00224-007-9027-4","volume":"43","author":"H. Schwichtenberg","year":"2008","unstructured":"Schwichtenberg, H.: Realizability interpretation of proofs in constructive analysis. Theory Comput. Syst. 43(3\u20134), 583\u2013602 (2008)","journal-title":"Theory Comput. Syst."},{"key":"9325_CR23","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","first-page":"338","DOI":"10.1007\/BFb0054298","volume-title":"Mathematics of Program Construction","author":"M. Tatsuta","year":"1998","unstructured":"Tatsuta, M.: Realizability of monotone coinductive definitions and its application to program synthesis. In: Parikh, R. (ed.) Mathematics of Program Construction. Lecture Notes in Mathematics, vol. 1422, pp. 338\u2013364. Springer, Berlin (1998)"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-011-9325-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-011-9325-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-011-9325-8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,6,9]],"date-time":"2019-06-09T20:23:33Z","timestamp":1560111813000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s00224-011-9325-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,4,14]]},"references-count":23,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2012,10]]}},"alternative-id":["9325"],"URL":"https:\/\/doi.org\/10.1007\/s00224-011-9325-8","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2011,4,14]]}}}