{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:47:32Z","timestamp":1759146452656,"version":"3.41.2"},"reference-count":35,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,3,24]],"date-time":"2011-03-24T00:00:00Z","timestamp":1300924800000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Based on a new coinductive characterization of continuous functions we\nextract certified programs for exact real number computation from constructive\nproofs. The extracted programs construct and combine exact real number\nalgorithms with respect to the binary signed digit representation of real\nnumbers. The data type corresponding to the coinductive definition of\ncontinuous functions consists of finitely branching non-wellfounded trees\ndescribing when the algorithm writes and reads digits. We discuss several\nexamples including the extraction of programs for polynomials up to degree two\nand the definite integral of continuous maps.<\/jats:p>","DOI":"10.2168\/lmcs-7(1:8)2011","type":"journal-article","created":{"date-parts":[[2011,9,23]],"date-time":"2011-09-23T12:18:47Z","timestamp":1316780327000},"source":"Crossref","is-referenced-by-count":12,"title":["From coinductive proofs to exact real arithmetic: theory and applications"],"prefix":"10.46298","volume":"Volume 7, Issue 1","author":[{"given":"Ulrich","family":"Berger","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2011,3,24]]},"reference":[{"key":"10.2168\/LMCS-7(1:8)2011_AbramskyJung94","unstructured":"Abramsky, S., Jung, A.: Domain theory. In Abramsky, S., Gabbay, D.M., Maibaum, T.S.E., eds.: Handbook of Logic in Computer Science, Volume 3. Clarendon Press (1994) 1-168"},{"key":"10.2168\/LMCS-7(1:8)2011_AbelMatthesUustalu05","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2004.10.017"},{"key":"10.2168\/LMCS-7(1:8)2011_AmadioBruceLongo86","unstructured":"Amadio, R., Bruce K., Longo, G.: The finitary projection model for second order lambda calculus and the solutions to higher order domain equations. In Proceedings of the First Annual IEEE Symposium on Logic in Computer Science (1986) 122-130."},{"key":"10.2168\/LMCS-7(1:8)2011_BenlBergerSchwichtenbergSeisenbergerZuber98","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 - A Basis for Applications. Volume II of Applied Logic Series. Kluwer, Dordrecht (1998) 41-71"},{"key":"10.2168\/LMCS-7(1:8)2011_Berger93","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(93)90038-F"},{"key":"10.2168\/LMCS-7(1:8)2011_BergerCSL09","unstructured":"Berger, U.: From coinductive proofs to exact real arithmetic. In Gr\u00e4del, E. and Kahle, R. eds.: Computer Science Logic. Volume 5771 of Lecture Notes in Computer Science., Springer (2009) 132-146"},{"key":"10.2168\/LMCS-7(1:8)2011_BergerCCA09","unstructured":"Berger, U.: Realisability and Adequacy for (Co)induction. In Bauer, A., Hertling P., Ko, K-I. eds.: 6th Int'l Conf. on Computability and Complexity in Analysis (Ljubljana). To appear: Journal of Universal Computer Science. Preliminary version available from Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik, Germany. http:\/\/drops.dagstuhl.de\/opus\/volltexte\/2009\/2258, 2009."},{"key":"10.2168\/LMCS-7(1:8)2011_BergerHou07","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-007-9017-6"},{"key":"10.2168\/LMCS-7(1:8)2011_BergerSeisenberger05","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. Volume 48 of Oxford Logic Guides. Oxford University Press (2005) 137-148"},{"key":"10.2168\/LMCS-7(1:8)2011_SeisenBerger10","unstructured":"Berger, U., Seisenberger, M.: Proofs, programs, processes. In Ferreira, F., L\u00f6we, B., Mayordomo, E. and Mendes Gomes, L., eds.: Computability in Europe. Volume 6158 of Lecture Notes in Computer Science, Springer (2010) 39-48"},{"key":"10.2168\/LMCS-7(1:8)2011_Bertot07","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005809"},{"key":"10.2168\/LMCS-7(1:8)2011_Blanck05","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2004.07.004"},{"key":"10.2168\/LMCS-7(1:8)2011_BradfieldStirling07","unstructured":"Bradfield, J., Stirling, C.: Modal mu-calculi. In Blackburn, P., van Benthem, J., Wolter, F., eds.: Handbook of Modal Logic. Volume 3 of Studies in Logic and Practical Reasoning. Elsevier (2007) 721-756"},{"key":"10.2168\/LMCS-7(1:8)2011_BuFePoSi81","doi-asserted-by":"crossref","unstructured":"Buchholz, W., Feferman, F., Pohlers, W., Sieg, W.: Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof-Theoretical Studies. Volume 897 of Lecture Notes in Mathematics. Springer, Berlin (1981)","DOI":"10.1007\/BFb0091894"},{"key":"10.2168\/LMCS-7(1:8)2011_CaprettaUustaluVene06","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2005.08.005"},{"key":"10.2168\/LMCS-7(1:8)2011_CiaffaglioneGianantonio06","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.09.061"},{"key":"10.2168\/LMCS-7(1:8)2011_EdalatHeckmann02","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 - Lecture Notes from the International Summer School, Caminha, Portugal. Springer (2002) 193-267"},{"key":"10.2168\/LMCS-7(1:8)2011_EscardoMarcial-Romero07","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.01.021"},{"key":"10.2168\/LMCS-7(1:8)2011_GeuversNiquiSpittersWiedijk07","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005834"},{"key":"10.2168\/LMCS-7(1:8)2011_GierzHofmannKeimelLawsonMisloveScott03","doi-asserted-by":"crossref","unstructured":"Gierz, G., Hofmann, K., Keimel, K., Lawson, J., Mislove, M., Scott, D.: Continuous Lattices and Domains. Volume 93 of Encyclopedia of Mathematics and its Applications. Cambridge University Press (2003)","DOI":"10.1017\/CBO9780511542725"},{"key":"10.2168\/LMCS-7(1:8)2011_Ghanietal09","doi-asserted-by":"crossref","unstructured":"Ghani, N., Hancock, P., Pattinson, D.: Representations of Stream Processors Using Nested Fixed Points. Logical Methods in Computer Science 5 (2009)","DOI":"10.2168\/LMCS-5(3:9)2009"},{"key":"10.2168\/LMCS-7(1:8)2011_Ghanietal09a","unstructured":"Ghani, N., Hancock, P., Pattinson, D.: Continuous functions on final coalgebras. Electr. Notes in Theoret. Comp. Sci. 249, 8 (2009) 3-18"},{"key":"10.2168\/LMCS-7(1:8)2011_HancockSetzer03","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, Oxford, Clarendon Press (2005) 115 - 134"},{"key":"10.2168\/LMCS-7(1:8)2011_Ko91","doi-asserted-by":"crossref","unstructured":"Ko, K-I.: Computational Complexity of Real Functions. Birkhauser Boston, Boston, MA (1991)","DOI":"10.1007\/978-1-4684-6802-1"},{"key":"10.2168\/LMCS-7(1:8)2011_Konecny04","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2003.11.015"},{"key":"10.2168\/LMCS-7(1:8)2011_Kreisel59","unstructured":"Kreisel, G.: Interpretation of analysis by means of constructive functionals of finite types. Constructivity in Mathematics (1959) 101-128"},{"key":"10.2168\/LMCS-7(1:8)2011_Lambov07","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129506005822"},{"key":"10.2168\/LMCS-7(1:8)2011_Malcolm90","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(90)90023-7"},{"key":"10.2168\/LMCS-7(1:8)2011_Mueller01","unstructured":"M\u00fcller, N.: The iRRAM: Exact Arithmetic in C++. In Blanck, J. and Brattka, V. and Hertling, P. eds.: Computability and Complexity in Analysis, (CCA'2000). Volume 2064 of Lecture Notes in Computer Science., Springer (2001) 22-252"},{"key":"10.2168\/LMCS-7(1:8)2011_Niqui08","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-4(3:6)2008"},{"key":"10.2168\/LMCS-7(1:8)2011_Plume98","unstructured":"Plume, D.: A Calculator for Exact Real Number Computation. PhD thesis, University of Edinburgh (1998)"},{"key":"10.2168\/LMCS-7(1:8)2011_Schwichtenberg08","doi-asserted-by":"publisher","DOI":"10.1007\/s00224-007-9027-4"},{"key":"10.2168\/LMCS-7(1:8)2011_Scriven08","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.10.020"},{"key":"10.2168\/LMCS-7(1:8)2011_Simpson98","unstructured":"Simpson, A.: Lazy Functional Algorithms for Exact Real Functionals. In: Mathematical Foundations of Computer Science. Volume 1450 of Lecture Notes in Computer Science, Springer (1998) 456-464"},{"key":"10.2168\/LMCS-7(1:8)2011_Tatsuta98","unstructured":"Tatsuta, M.: Realizability of monotone coinductive definitions and its application to program synthesis. In Parikh, R., ed.: Mathematics of Program Construction. Volume 1422 of Lecture Notes in Mathematics, Springer (1998) 338-364"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1109\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1109\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:03:33Z","timestamp":1681243413000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1109"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,3,24]]},"references-count":35,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(1:8)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1101.2162","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1101.2162","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2011,3,24]]},"article-number":"1109"}}