{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,8,31]],"date-time":"2025-08-31T10:13:15Z","timestamp":1756635195899},"reference-count":20,"publisher":"Springer Science and Business Media LLC","issue":"3-4","license":[{"start":{"date-parts":[[2007,7,27]],"date-time":"2007-07-27T00:00:00Z","timestamp":1185494400000},"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-9017-6","type":"journal-article","created":{"date-parts":[[2007,7,26]],"date-time":"2007-07-26T11:56:01Z","timestamp":1185450961000},"page":"394-409","source":"Crossref","is-referenced-by-count":8,"title":["Coinduction for Exact Real Number Computation"],"prefix":"10.1007","volume":"43","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tie","family":"Hou","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2007,7,27]]},"reference":[{"key":"9017_CR1","unstructured":"Bertot, Y.: Coinduction in Coq. In: Lecture Notes of TYPES Summer School 2005, Sweden, vol. II (2005)"},{"issue":"1","key":"9017_CR2","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. Struc. Comput. Sci. 17(1), 37\u201363 (2007)","journal-title":"Math. Struc. Comput. Sci."},{"key":"9017_CR3","doi-asserted-by":"crossref","first-page":"75","DOI":"10.1016\/j.apal.2005.05.006","volume":"136","author":"W. Buchholz","year":"2005","unstructured":"Buchholz, W.: A term calculus for (co-)recursive definitions on streamlike data-structures. Ann. Pure Appl. Log. 136, 75\u201390 (2005)","journal-title":"Ann. Pure Appl. Log."},{"key":"9017_CR4","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., Gianantonio, Di P.: A certified, corecursive implementation of exact real numbers. Theor. Comput. Sci. 351, 39\u201351 (2006)","journal-title":"Theor. Comput. Sci."},{"key":"9017_CR5","doi-asserted-by":"crossref","unstructured":"Chirimar, J., Howe, D.J.: Implementing constructive real analysis: preliminary report. In: Lecture Notes in Comput. Sci., vol. 613, pp.\u00a0165\u2013178 (1992)","DOI":"10.1007\/BFb0021090"},{"key":"9017_CR6","first-page":"193","volume-title":"International Summer School on Applied Semantics, Caminha, Portugal","author":"A. Edalat","year":"2002","unstructured":"Edalat, A., Heckmann, R.: Computing with real numbers\u2014I. The LFT approach to real number computation\u2014II. A domain framework for computational geometry. In: Barthe, G., Dybjer, P., Pinto, L., Saraiva, J. (eds.) International Summer School on Applied Semantics, Caminha, Portugal, pp. 193\u2013267. Springer, Berlin (2002)"},{"key":"9017_CR7","doi-asserted-by":"crossref","unstructured":"Edalat, A., Potts, P.J.: A new representation for exact real numbers. In: Brooks, S., Mislove, M. (eds.) Mathematical Foundations of Programming Semantics (MFPS XIII), Carnegie Mellon, Pittsburgh, PA, USA. Electron. Notes Theor. Comput. Sci. (1997)","DOI":"10.1016\/S1571-0661(05)80166-5"},{"key":"9017_CR8","doi-asserted-by":"crossref","unstructured":"Gibbons, J.: Streaming representation-changers. In: Lecture Notes in Comput. Sci., vol. 3125, pp.\u00a0142\u2013168 (2004)","DOI":"10.1007\/978-3-540-27764-4_9"},{"key":"9017_CR9","first-page":"222","volume":"62","author":"B. Jacobs","year":"1997","unstructured":"Jacobs, B., Rutten, J.: A tutorial on (co)algebras and (co)induction. EATCS Bull. 62, 222\u2013259 (1997)","journal-title":"EATCS Bull."},{"key":"9017_CR10","doi-asserted-by":"crossref","DOI":"10.1007\/978-1-4684-6802-1","volume-title":"Complexity Theory of Real Functions","author":"K.-I. Ko","year":"1991","unstructured":"Ko, K.-I.: Complexity Theory of Real Functions. Birkh\u00e4user, Boston (1991)"},{"key":"9017_CR11","doi-asserted-by":"crossref","unstructured":"Lenisa, M.: From set-theoretic coinduction to coalgebraic coinduction: some results, some problems. In: Jacobs, B., Rutten, J. (eds.) Coalgebraic Methods in Computer Science CMCS\u201999 Conference Proceedings. Electron. Notes Theor. Comput. Sci., vol. 19 (1999)","DOI":"10.1016\/S1571-0661(05)80265-8"},{"key":"9017_CR12","doi-asserted-by":"crossref","unstructured":"Niqui, M.: Formalising exact arithmetic in type theory. In: Cooper, S.B., L\u00f6we, B., Torenvliet, L. (eds.) New Computational Paradigms: First Conference on Computability in Europe, CiE 2005, Amsterdam, The Netherlands, June 8\u201312, 2005, Proceedings. Lecture Notes in Comput. Sci., vol. 3526, pp.\u00a0368\u2013377 (2005)","DOI":"10.1007\/11494645_46"},{"key":"9017_CR13","unstructured":"Niqui, M.: Coinductive correctness of homographic and quadratic algorithms for exact real numbers. In: Altenkirch, T., McBride, C. (eds.) Proceedings of TYPES 2006 Workshop. Lecture Notes in Comput. Sci. (2007, to appear)"},{"key":"9017_CR14","unstructured":"Plume, D.: A calculator for exact real number computation, 4th year project. Departments of Computer Science and Artificial Intelligence, University of Edinburgh (1998)"},{"key":"9017_CR15","doi-asserted-by":"crossref","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"J. Rutten","year":"2000","unstructured":"Rutten, J.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249, 3\u201380 (2000)","journal-title":"Theor. Comput. Sci."},{"key":"9017_CR16","doi-asserted-by":"crossref","unstructured":"Schwichtenberg, H.: Inverting monotone continuous functions in constructive analysis. In: Beckmann, A., Berger, U., L\u00f6we, B. (eds.) Logical Approaches to Computational Barriers: Second Conference on Computability in Europe, CiE 2006, Swansea, UK, June 30\u2013July 5, 2006. Lecture Notes in Comput. Sci., vol. 3988, pp.\u00a0490\u2013504 (2006)","DOI":"10.1007\/11780342_50"},{"key":"9017_CR17","doi-asserted-by":"crossref","unstructured":"Tatsuta, M.: Realizability of monotone coinductive definitions and its application to program synthesis. In: Proceedings of the Fourth International Conference on Mathematics of Program Construction. Lecture Notes in Comput. Sci., vol. 1422, pp.\u00a0338\u2013364 (1998)","DOI":"10.1007\/BFb0054298"},{"key":"9017_CR18","unstructured":"Telford, A., Turner, D.: Ensuring the productivity of infinite structures. Technical Report 551, University of Kent at Canterbury (1997)"},{"key":"9017_CR19","doi-asserted-by":"crossref","first-page":"161","DOI":"10.1112\/plms\/s2-45.1.161","volume":"45","author":"A.M. Turing","year":"1939","unstructured":"Turing, A.M.: Systems of logic based on ordinals. Proc. Lond. Math. Soc. 45, 161\u2013228 (1939)","journal-title":"Proc. Lond. Math. Soc."},{"key":"9017_CR20","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-642-56999-9","volume-title":"Computable Analysis, an Introduction","author":"K. Weihrauch","year":"2000","unstructured":"Weihrauch, K.: Computable Analysis, an Introduction. Springer, New York (2000)"}],"container-title":["Theory of Computing Systems"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9017-6.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s00224-007-9017-6\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s00224-007-9017-6","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-9017-6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,7,27]]},"references-count":20,"journal-issue":{"issue":"3-4","published-print":{"date-parts":[[2008,12]]}},"alternative-id":["9017"],"URL":"https:\/\/doi.org\/10.1007\/s00224-007-9017-6","relation":{},"ISSN":["1432-4350","1433-0490"],"issn-type":[{"value":"1432-4350","type":"print"},{"value":"1433-0490","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,7,27]]}}}