{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,3,19]],"date-time":"2025-03-19T14:24:41Z","timestamp":1742394281016},"reference-count":40,"publisher":"Cambridge University Press (CUP)","issue":"1","license":[{"start":{"date-parts":[[2007,2,1]],"date-time":"2007-02-01T00:00:00Z","timestamp":1170288000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2007,2]]},"abstract":"<jats:p>We extend the work of A. Ciaffaglione and P. di Gianantonio on the mechanical verification of algorithms for exact computation on real numbers, using infinite streams of digits implemented as a co-inductive type. Four aspects are studied. The first concerns the proof that digit streams correspond to axiomatised real numbers when they are already present in the proof system. The second re-visits the definition of an addition function, looking at techniques to let the proof search engine perform the effective construction of an algorithm that is correct by construction. The third concerns the definition of a function to compute affine formulas with positive rational coefficients. This is an example where we need to combine co-recursion and recursion. Finally, the fourth aspect concerns the definition of a function to compute series, with an application on the series that is used to compute Euler's number <jats:italic>e<\/jats:italic>. All these experiments should be reproducible in any proof system that supports co-inductive types, co-recursion and general forms of terminating recursion; we used the C<jats:sc>OQ<\/jats:sc> system (Dowek <jats:italic>et al<\/jats:italic>. 1993; Bertot and Cast\u00e9ran 2004; Gim\u00e9nez 1994).<\/jats:p>","DOI":"10.1017\/s0960129506005809","type":"journal-article","created":{"date-parts":[[2007,3,7]],"date-time":"2007-03-07T10:59:58Z","timestamp":1173265198000},"page":"37-63","source":"Crossref","is-referenced-by-count":12,"title":["Affine functions and series with co-inductive real numbers"],"prefix":"10.1017","volume":"17","author":[{"given":"YVES","family":"BERTOT","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"56","published-online":{"date-parts":[[2007,2,1]]},"reference":[{"key":"S0960129506005809_rf31","doi-asserted-by":"publisher","DOI":"10.1007\/11532231_22"},{"key":"S0960129506005809_rf15","volume-title":"The Coq Proof Assistant User's Guide","author":"Dowek","year":"1993"},{"key":"S0960129506005809_rf23","first-page":"265","volume-title":"FMCAD","author":"Harrison","year":"1996"},{"key":"S0960129506005809_rf10","first-page":"88","volume-title":"MKM","author":"Cruz-Filipe","year":"2004"},{"key":"S0960129506005809_rf14","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-39185-1_9"},{"key":"S0960129506005809_rf12","volume-title":"Proceedings of JFLA'2001","author":"Delahaye","year":"2001"},{"key":"S0960129506005809_rf38","volume-title":"Proceedings of the conference Typed Lambda Calculi and Applications","author":"Paulin-Mohring","year":"1993"},{"key":"S0960129506005809_rf11","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-44755-5_13"},{"key":"S0960129506005809_rf18","first-page":"39","volume-title":"Types for proofs and Programs","author":"Gim\u00e9nez","year":"1994"},{"key":"S0960129506005809_rf36","unstructured":"Niqui M. (2004) Formalising Exact Arithmetic, Representations, Algorithms, and Proofs, Ph.D. thesis, University of Nijmegen, ISBN 90-9018333-7."},{"key":"S0960129506005809_rf30","unstructured":"Mayero M. (2001) Formalisation et automatisation de preuves en analyses r\u00e9elle et num\u00e9rique, Ph.D. thesis, Universit\u00e9 Paris VI."},{"key":"S0960129506005809_rf1","first-page":"489","volume-title":"Automata, languages and programming","author":"Bauer","year":"2002"},{"key":"S0960129506005809_rf4","first-page":"162","volume-title":"LISP and Functional Programming","author":"Boehm","year":"1986"},{"key":"S0960129506005809_rf8","first-page":"114","volume-title":"Types 1999 Workshop, L\u00f6keberg, Sweden","author":"Ciaffaglione","year":"2000"},{"key":"S0960129506005809_rf16","volume-title":"Electronic Notes in Theoretical Computer Science","author":"Edalat","year":"1998"},{"key":"S0960129506005809_rf24","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-1591-5"},{"key":"S0960129506005809_rf19","unstructured":"Gosper R. W. (1972) HAKMEM, Item 101 B. MIT AI Laboratory Memo No.239. Available at http:\/\/www.inwap.com\/pdp10\/hbaker\/hakmem\/cf.html#item101b."},{"key":"S0960129506005809_rf6","unstructured":"Boldo S. , Daumas M. , Moreau-Finot C. and Th\u00e9ry L. (2002) Computer validated proofs of a toolset for adaptable arithmetic. Submitted to Journal of the ACM."},{"key":"S0960129506005809_rf39","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008669628911"},{"key":"S0960129506005809_rf27","unstructured":"Lambov B. (2005) Reallib: an efficient implementation of exact real arithmetic. In: Grubba T. , Hertling P. , Tsuiki H. and Weihrauch K. (eds.) CCA 2005 \u2013 Second International Conference on Computability and Complexity in Analysis, August 25\u201329, 2005, Kyoto, Japan. Informatik Berichte 326-7\/2005, Fern Universit\u00e4t Hagen, Germany 169\u2013175."},{"key":"S0960129506005809_rf20","first-page":"440","article-title":"Cannonballs and honeycombs","volume":"47","author":"Hales","year":"2000","journal-title":"Notices of the AMS"},{"key":"S0960129506005809_rf2","doi-asserted-by":"publisher","DOI":"10.1007\/11417170_9"},{"key":"S0960129506005809_rf28","doi-asserted-by":"crossref","unstructured":"Mahboubi A. (2007) Implementing the Cylindrical Algebraic Decomposition inside the Coq system. Mathematical Structures in Computer Science, this issue.","DOI":"10.1017\/S096012950600586X"},{"key":"S0960129506005809_rf25","first-page":"234","volume-title":"Theorem Proving in Higher Order Logics: 13th International Conference, TPHOLs 2000","author":"Harrison","year":"2000"},{"key":"S0960129506005809_rf26","first-page":"9","article-title":"IEEE standard for binary floating-point arithmetic","volume":"22","year":"1987","journal-title":"SIGPLAN Notices"},{"key":"S0960129506005809_rf13","unstructured":"di Gianantonio P. (1996) A golden ration notation for the real numbers. Technical Report CS-R9602, CWI, Amsterdam."},{"key":"S0960129506005809_rf40","doi-asserted-by":"publisher","DOI":"10.1109\/12.57047"},{"key":"S0960129506005809_rf29","volume-title":"Journ\u00e9es Francophones des Langages Applicatifs","author":"Mahboubi","year":"2002"},{"key":"S0960129506005809_rf3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"S0960129506005809_rf33","unstructured":"M\u00e9nissier-Morain V. (1995) Conception et algorithmique d'une repr\u00e9sentation d'arithm\u00e9tique r\u00e9elle en pr\u00e9cision arbitraire. In: Proceedings of the first conference on real numbers and computers."},{"key":"S0960129506005809_rf34","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-2646-6"},{"key":"S0960129506005809_rf37","doi-asserted-by":"publisher","DOI":"10.1007\/BF01941137"},{"key":"S0960129506005809_rf17","first-page":"142","volume-title":"MPC","author":"Gibbons","year":"2004"},{"key":"S0960129506005809_rf5","unstructured":"Boldo S. (2004) Preuves formelles en arithm\u00e9tiques \u00e0 virgule flottante, Ph.D. thesis, \u00c9cole Normale Sup'erieure de Lyon."},{"key":"S0960129506005809_rf32","unstructured":"M\u00e9nissier-Morain V. (1994) Arithm\u00e9tique exacte, conception, algorithmique et performances d'une impl\u00e9mentation informatique en pr\u00e9cision arbitraire, Th\u00e8se, Universit\u00e9 Paris 7."},{"key":"S0960129506005809_rf22","unstructured":"Hanrot G. , Lef\u00e8vre V. , P\u00e9lissier P. and Zimmermann P. (2000) The mpfr library. Available at http:\/\/www.mpfr.org."},{"key":"S0960129506005809_rf35","unstructured":"M\u00fcller N. T. (2005) Implementing exact real numbers efficiently. In: Grubba T. , Hertling P. , Tsuiki H. and Weihrauch K. (eds.) CCA 2005 \u2013 Second International Conference on Computability and Complexity in Analysis, August 25\u201329, 2005, Kyoto, Japan. Informatik Berichte 326\u20137\/2005, Fern Universit\u00e4t Hagen, Germany 378."},{"key":"S0960129506005809_rf9","first-page":"62","volume-title":"Types for Proofs and Programs","author":"Coquand","year":"1993"},{"key":"S0960129506005809_rf21","unstructured":"Hales T. (2004) The flyspeck project fact sheet. Available at http:\/\/www.math.pitt.edu\/~thales\/flyspeck\/index.html"},{"key":"S0960129506005809_rf7","volume-title":"Springer-Verlag Lecture Notes in Computer Science","author":"Boutin","year":"1997"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129506005809","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,4,1]],"date-time":"2019-04-01T18:54:00Z","timestamp":1554144840000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129506005809\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2007,2]]},"references-count":40,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2007,2]]}},"alternative-id":["S0960129506005809"],"URL":"https:\/\/doi.org\/10.1017\/s0960129506005809","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2007,2]]}}}