{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,5]],"date-time":"2025-10-05T04:33:14Z","timestamp":1759638794096},"publisher-location":"Berlin, Heidelberg","reference-count":26,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642040269"},{"type":"electronic","value":"9783642040276"}],"license":[{"start":{"date-parts":[[2009,1,1]],"date-time":"2009-01-01T00:00:00Z","timestamp":1230768000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2009]]},"DOI":"10.1007\/978-3-642-04027-6_12","type":"book-chapter","created":{"date-parts":[[2009,9,14]],"date-time":"2009-09-14T17:27:52Z","timestamp":1252949272000},"page":"132-146","source":"Crossref","is-referenced-by-count":5,"title":["From Coinductive Proofs to Exact Real Arithmetic"],"prefix":"10.1007","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[]}],"member":"297","reference":[{"key":"12_CR1","first-page":"120","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.\u00a0Comput.\u00a0Sci.\u00a0379, 120\u2013141 (2007)","journal-title":"Theor.\u00a0Comput.\u00a0Sci."},{"key":"12_CR2","doi-asserted-by":"publisher","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.\u00a0Struct.\u00a0Comput.\u00a0Sci.\u00a017, 3\u201336 (2007)","journal-title":"Math.\u00a0Struct.\u00a0Comput.\u00a0Sci."},{"key":"12_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"193","DOI":"10.1007\/3-540-45699-6_5","volume-title":"Applied Semantics","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.) APPSEM 2000. LNCS, vol.\u00a02395, pp. 193\u2013267. Springer, Heidelberg (2002)"},{"key":"12_CR4","first-page":"39","volume":"351","author":"A. Ciaffaglione","year":"2006","unstructured":"Ciaffaglione, A., Di Gianantonio, P.: A certified, corecursive implementation of exact real numbers. Theor.\u00a0Comput.\u00a0Sci.\u00a0351, 39\u201351 (2006)","journal-title":"Theor.\u00a0Comput.\u00a0Sci."},{"key":"12_CR5","doi-asserted-by":"publisher","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.\u00a0Struct.\u00a0Comput.\u00a0Sci.\u00a017, 37\u201363 (2007)","journal-title":"Math.\u00a0Struct.\u00a0Comput.\u00a0Sci."},{"key":"12_CR6","unstructured":"Berger, U., Hou, T.: Coinduction for exact real number computation. Theory Comput.\u00a0Sys. (to appear, 2009)"},{"key":"12_CR7","doi-asserted-by":"publisher","first-page":"1","DOI":"10.2168\/LMCS-4(3:6)2008","volume":"4","author":"M. Niqui","year":"2008","unstructured":"Niqui, M.: Coinductive formal reasoning in exact real arithmetic. Logical Methods in Computer Science\u00a04, 1\u201340 (2008)","journal-title":"Logical Methods in Computer Science"},{"key":"12_CR8","unstructured":"Schwichtenberg, H.: Realizability interpretation of proofs in constructive analysis. Theory Comput.\u00a0Sys. (to appear, 2009)"},{"key":"12_CR9","series-title":"Oxford Logic Guides","doi-asserted-by":"publisher","first-page":"137","DOI":"10.1093\/acprof:oso\/9780198566519.003.0008","volume-title":"From Sets and Types to Topology and Analysis Towards practicable foundations for constructive mathematics","author":"U. Berger","year":"2005","unstructured":"Berger, U., Seisenberger, M.: Applications of inductive definitions and choice principles to program synthesis. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis Towards practicable foundations for constructive mathematics. Oxford Logic Guides, vol.\u00a048, pp. 137\u2013148. Oxford University Press, Oxford (2005)"},{"key":"12_CR10","doi-asserted-by":"crossref","unstructured":"Ghani, N., Hancock, P., Pattinson, D.: Continuous functions on final coalgebras. Electr. Notes in Theoret. Comp. Sci.\u00a0164 (2006)","DOI":"10.1016\/j.entcs.2006.06.009"},{"key":"12_CR11","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","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":"12_CR12","series-title":"Studies in Logic and Practical Reasoning","doi-asserted-by":"publisher","first-page":"721","DOI":"10.1016\/S1570-2464(07)80015-2","volume-title":"Handbook of Modal Logic","author":"J. Bradfield","year":"2007","unstructured":"Bradfield, J., Stirling, C.: Modal mu-calculi. In: Blackburn, P., van Benthem, J., Wolter, F. (eds.) Handbook of Modal Logic. Studies in Logic and Practical Reasoning, vol.\u00a03, pp. 721\u2013756. Elsevier, Amsterdam (2007)"},{"key":"12_CR13","series-title":"Encyclopedia of Mathematics and its Applications","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511542725","volume-title":"Continuous Lattices and Domains","author":"G. Gierz","year":"2003","unstructured":"Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M., Scott, D.: Continuous Lattices and Domains. Encyclopedia of Mathematics and its Applications, vol.\u00a093. Cambridge University Press, Cambridge (2003)"},{"key":"12_CR14","unstructured":"Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. Constructivity in Mathematics, 101\u2013128 (1959)"},{"key":"12_CR15","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","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: Jeuring, J. (ed.) MPC 1998. Lecture Notes in Mathematics, vol.\u00a01422, pp. 338\u2013364. Springer, Heidelberg (1998)"},{"key":"12_CR16","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"crossref","DOI":"10.1007\/BFb0066739","volume-title":"Metamathematical Investigation of Intuitionistic Arithmetic and Analysis","author":"A. Troelstra","year":"1973","unstructured":"Troelstra, A.: Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. Lecture Notes in Mathematics, vol.\u00a0344. Springer, Heidelberg (1973)"},{"key":"12_CR17","first-page":"1","volume-title":"Handb.\u00a0Logic\u00a0Comput.\u00a0Sci.","author":"S. Abramsky","year":"1994","unstructured":"Abramsky, S., Jung, A.: Domain theory. In: Abramsky, S., Gabbay, D.M., Maibaum, T.S.E. (eds.) Handb.\u00a0Logic\u00a0Comput.\u00a0Sci., vol.\u00a03, pp. 1\u2013168. Clarendon Press, Oxford (1994)"},{"key":"12_CR18","doi-asserted-by":"publisher","first-page":"255","DOI":"10.1016\/0167-6423(90)90023-7","volume":"14","author":"G. Malcolm","year":"1990","unstructured":"Malcolm, G.: Data structures and program transformation. Science of Computer Programming\u00a014, 255\u2013279 (1990)","journal-title":"Science of Computer Programming"},{"key":"12_CR19","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1093\/acprof:oso\/9780198566519.003.0007","volume-title":"From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics","author":"P. Hancock","year":"2005","unstructured":"Hancock, P., Setzer, A.: Guarded induction and weakly final coalgebras in dependent type theory. In: Crosilla, L., Schuster, P. (eds.) From Sets and Types to Topology and Analysis. Towards Practicable Foundations for Constructive Mathematics, pp. 115\u2013134. Clarendon Press, Oxford (2005)"},{"key":"12_CR20","first-page":"3","volume":"333","author":"A. Abel","year":"2005","unstructured":"Abel, A., Matthes, R., Uustalu, T.: Iteration and coiteration schemes for higher-order and nested datatypes. Theor.\u00a0Comput.\u00a0Sci.\u00a0333, 3\u201366 (2005)","journal-title":"Theor.\u00a0Comput.\u00a0Sci."},{"key":"12_CR21","doi-asserted-by":"publisher","first-page":"437","DOI":"10.1016\/j.ic.2005.08.005","volume":"204","author":"V. Capretta","year":"2006","unstructured":"Capretta, V., Uustalu, T., Vene, V.: Recursive coalgebras from comonads. Information and Computation\u00a0204, 437\u2013468 (2006)","journal-title":"Information and Computation"},{"key":"12_CR22","first-page":"109","volume":"315","author":"M. Kone\u010dn\u00fd","year":"2004","unstructured":"Kone\u010dn\u00fd, M.: Real functions incrementally computable by finite automata. Theor.\u00a0Comput.\u00a0Sci.\u00a0315, 109\u2013133 (2004)","journal-title":"Theor.\u00a0Comput.\u00a0Sci."},{"key":"12_CR23","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1016\/j.jlap.2004.07.004","volume":"64","author":"J. Blanck","year":"2005","unstructured":"Blanck, J.: Efficient exact computation of iterated maps. Journal of Logic and Algebraic Programming\u00a064, 41\u201359 (2005)","journal-title":"Journal of Logic and Algebraic Programming"},{"key":"12_CR24","unstructured":"Plume, D.: A Calculator for Exact Real Number Computation. PhD thesis. University of Edinburgh (1998)"},{"key":"12_CR25","series-title":"Applied Logic Series","doi-asserted-by":"publisher","first-page":"41","DOI":"10.1007\/978-94-017-0435-9_2","volume-title":"Automated Deduction \u2013 A 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. (eds.) Automated Deduction \u2013 A Basis for Applications. Applied Logic Series, vol.\u00a0II, pp. 41\u201371. Kluwer, Dordrecht (1998)"},{"key":"12_CR26","doi-asserted-by":"publisher","first-page":"337","DOI":"10.1016\/j.entcs.2008.10.020","volume":"218","author":"A. Scriven","year":"2008","unstructured":"Scriven, A.: A functional algorithm for exact real integration with invariant measures. Electron. Notes Theor. Comput. Sci.\u00a0218, 337\u2013353 (2008)","journal-title":"Electron. Notes Theor. Comput. Sci."}],"container-title":["Lecture Notes in Computer Science","Computer Science Logic"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-04027-6_12","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,22]],"date-time":"2019-05-22T15:19:26Z","timestamp":1558538366000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-04027-6_12"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009]]},"ISBN":["9783642040269","9783642040276"],"references-count":26,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-04027-6_12","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2009]]}}}