{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,2,21]],"date-time":"2025-02-21T07:34:40Z","timestamp":1740123280254,"version":"3.37.3"},"reference-count":39,"publisher":"Springer Science and Business Media LLC","issue":"1-4","license":[{"start":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T00:00:00Z","timestamp":1513728000000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"funder":[{"name":"ANR Agence Nationale de La Recherche","award":["ANR-14-CE25-0018-01"],"award-info":[{"award-number":["ANR-14-CE25-0018-01"]}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["J Autom Reasoning"],"published-print":{"date-parts":[[2018,6]]},"DOI":"10.1007\/s10817-017-9444-2","type":"journal-article","created":{"date-parts":[[2017,12,20]],"date-time":"2017-12-20T05:43:50Z","timestamp":1513748630000},"page":"33-71","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":0,"title":["Distant Decimals of $$\\pi $$ \u03c0 : Formal Proofs of Some Algorithms Computing Them and Guarantees of Exact Computation"],"prefix":"10.1007","volume":"61","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-5052-3019","authenticated-orcid":false,"given":"Yves","family":"Bertot","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurence","family":"Rideau","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Laurent","family":"Th\u00e9ry","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2017,12,20]]},"reference":[{"key":"9444_CR1","first-page":"125","volume-title":"Gauss, Landen, Ramanujan, the Arithmetic\u2013Geometric Mean, Ellipses, $$\\pi $$ \u03c0","author":"G Almkvist","year":"2016","unstructured":"Almkvist, G., Berndt, B.: Gauss, Landen, Ramanujan, the Arithmetic\u2013Geometric Mean, Ellipses, $$\\pi $$ \u03c0 , and the Ladies Diary (1988), pp. 125\u2013150. Springer, Berlin (2016)"},{"key":"9444_CR2","unstructured":"Anonymous: Premi\u00e8re composition de math\u00e9matiques\u201d, concours externe de recrutement de professeurs certifi\u00e9s, section math\u00e9matiques (1995)"},{"key":"9444_CR3","doi-asserted-by":"crossref","unstructured":"Armand, M., Gr\u00e9goire, B., Spiwack, A., Th\u00e9ry, L.: Extending Coq with imperative features and its application to SAT verification. In: Interactive Theorem Proving, First International Conference, ITP 2010, volume 6172 of LNCS. Springer, pp. 83\u201398 (2010)","DOI":"10.1007\/978-3-642-14052-5_8"},{"issue":"218","key":"9444_CR4","doi-asserted-by":"crossref","first-page":"903","DOI":"10.1090\/S0025-5718-97-00856-9","volume":"66","author":"D Bailey","year":"1997","unstructured":"Bailey, D.: Borwein, Peter, Plouffe, Simon: on the rapid computation of various polylogarithmic constants. Math. Comput. 66(218), 903\u2013913 (1997)","journal-title":"Math. Comput."},{"key":"9444_CR5","doi-asserted-by":"crossref","unstructured":"Bertot, Y.: Fixed precision patterns for the formal verification of mathematical constant approximations. In: Proceedings of the 2015 Conference on Certified Programs and Proofs. ACM, pp. 147\u2013155 (2015)","DOI":"10.1145\/2676724.2693172"},{"issue":"1","key":"9444_CR6","first-page":"105","volume":"7","author":"Y Bertot","year":"2014","unstructured":"Bertot, Y., Allais, G.: Views of Pi: definition and computation. J. Formaliz. Reason. 7(1), 105\u2013129 (2014)","journal-title":"J. Formaliz. Reason."},{"issue":"3\u20134","key":"9444_CR7","doi-asserted-by":"crossref","first-page":"225","DOI":"10.1023\/A:1021987403425","volume":"29","author":"Y Bertot","year":"2002","unstructured":"Bertot, Y., Magaud, N., Zimmermann, P.: A proof of GMP square root. J. Autom. Reason. 29(3\u20134), 225\u2013252 (2002)","journal-title":"J. Autom. Reason."},{"key":"9444_CR8","unstructured":"Bertot, Y., Rideau, L., Th\u00e9ry, L.: Distant decimals of pi. https:\/\/www-sop.inria.fr\/marelle\/distant-decimals-pi\/ (2017). Accessed 18 Dec 2017"},{"key":"9444_CR9","doi-asserted-by":"crossref","unstructured":"Besson, F.: Fast reflexive arithmetic tactics the linear case and beyond. In: Proceedings of the 2006 International Conference on Types for Proofs and Programs, volume 4502 of LNCS. Springer, pp. 48\u201362 (2007)","DOI":"10.1007\/978-3-540-74464-1_4"},{"key":"9444_CR10","doi-asserted-by":"crossref","unstructured":"Boespflug, M., D\u00e9n\u00e8s, M., Gr\u00e9goire, B.: Full reduction at full throttle. In Certified Programs and Proofs: First International Conference, volume 7086 of LNCS. Springer, pp. 362\u2013377 (2011)","DOI":"10.1007\/978-3-642-25379-9_26"},{"issue":"1","key":"9444_CR11","doi-asserted-by":"crossref","first-page":"41","DOI":"10.1007\/s11786-014-0181-1","volume":"9","author":"S Boldo","year":"2015","unstructured":"Boldo, S., Lelay, C., Melquiond, G.: Coquelicot: a user-friendly library of real analysis for Coq. Math. Comput. Sci. 9(1), 41\u201362 (2015)","journal-title":"Math. Comput. Sci."},{"key":"9444_CR12","doi-asserted-by":"crossref","unstructured":"Boldo, S., Melquiond, G.: Flocq: a unified library for proving floating-point algorithms in Coq. In: IEEE Symposium on Computer Arithmetic. IEEE Computer Society, pp. 243\u2013252 (2011)","DOI":"10.1109\/ARITH.2011.40"},{"key":"9444_CR13","volume-title":"Pi and the AGM: A Study in the Analytic Number Theory and Computational Complexity","author":"JM Borwein","year":"1987","unstructured":"Borwein, J.M., Borwein, P.B.: Pi and the AGM: A Study in the Analytic Number Theory and Computational Complexity. Wiley, New York (1987)"},{"issue":"2","key":"9444_CR14","doi-asserted-by":"crossref","first-page":"242","DOI":"10.1145\/321941.321944","volume":"23","author":"RP Brent","year":"1976","unstructured":"Brent, R.P.: Fast multiple-precision evaluation of elementary functions. J. ACM 23(2), 242\u2013251 (1976)","journal-title":"J. ACM"},{"key":"9444_CR15","first-page":"595","volume":"205","author":"H Cartan","year":"1937","unstructured":"Cartan, H.: Th\u00e9orie des filtres. Comptes Rendus de l\u2019Acad\u00e9mie des Sciences 205, 595\u2013598 (1937)","journal-title":"Comptes Rendus de l\u2019Acad\u00e9mie des Sciences"},{"key":"9444_CR16","doi-asserted-by":"crossref","unstructured":"Cohen, C., D\u00e9n\u00e8s, M., M\u00f6rtberg, A.: Refinements for free! In: Certified Programs and Proofs: Third International Conference, volume 8307 of LNCS. Springer, pp. 147\u2013162 (2013)","DOI":"10.1007\/978-3-319-03545-1_10"},{"key":"9444_CR17","unstructured":"Cruz-Filipe, L.: Constructive Real Analysis: A Type-Theoretical Formalization and Applications. PhD Thesis, University of Nijmegen, April (2004)"},{"key":"9444_CR18","doi-asserted-by":"crossref","unstructured":"D\u00e9n\u00e8s, M., M\u00f6rtberg, A., Siles, V.: A refinement-based approach to computational algebra in Coq. In: Interactive Theorem Proving\u2014Third International Conference, ITP 2012, volume 7406 of LNCS. Springer, pp. 83\u201398 (2012)","DOI":"10.1007\/978-3-642-32347-8_7"},{"key":"9444_CR19","unstructured":"Coq Development Team. The Coq proof assistant. http:\/\/coq.inria.fr (2016). Accessed 18 Dec 2017"},{"key":"9444_CR20","doi-asserted-by":"crossref","unstructured":"Filli\u00e2tre, J.-C., Paskevich, A.: Why3\u2014where programs meet provers. In: Programming Languages and Systems: 22nd European Symposium on Programming, ESOP 2013, volume 7792 of LNCS. Springer, pp. 125\u2013128 (2013)","DOI":"10.1007\/978-3-642-37036-6_8"},{"issue":"2","key":"9444_CR21","doi-asserted-by":"crossref","first-page":"13","DOI":"10.1145\/1236463.1236468","volume":"33","author":"L Fousse","year":"2007","unstructured":"Fousse, L., Hanrot, G., Lef\u00e8vre, V., P\u00e9lissier, P., Zimmermann, P.: MPFR: a multiple-precision binary floating-point library with correct rounding. ACM Trans. Math. Softw. 33(2), 13 (2007)","journal-title":"ACM Trans. Math. Softw."},{"key":"9444_CR22","unstructured":"Gonthier, G., et al: Mathematical components. http:\/\/math-comp.github.io\/math-comp\/ . Accessed 18 Dec 2017"},{"key":"9444_CR23","unstructured":"Gourevitch, B.: The world of Pi, 1999. http:\/\/www.pi314.net (2017). Accessed 18 Dec 2017"},{"key":"9444_CR24","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Th\u00e9ry, L.: A purely functional library for modular arithmetic and its application to certifying large prime numbers. In: Automated Reasoning: Third International Joint Conference, IJCAR 2006, volume 4130 of LNCS. Springer, pp. 423\u2013437 (2006)","DOI":"10.1007\/11814771_36"},{"key":"9444_CR25","unstructured":"Hales, T.C., et\u00a0al.: A formal proof of the Kepler conjecture. arXiv:1501.02155 (2015)"},{"key":"9444_CR26","unstructured":"Harrison, J.: Formalizing basic complex analysis. In: From Insight to Proof: Festschrift in Honour of Andrzej Trybulec, volume 10(23) of Studies in Logic, Grammar and Rhetoric. University of Bia\u0142ystok, pp. 151\u2013165. http:\/\/mizar.org\/trybulec65\/ (2007)"},{"key":"9444_CR27","unstructured":"Harrison, J.: Pi series in Bailey\/Borwein\/Plouffe polylogarithmic constants paper, the HOL Light library. https:\/\/github.com\/jrh13\/hol-light\/blob\/master\/Examples\/polylog.ml (2010). Accessed 18 Dec 2017"},{"key":"9444_CR28","volume-title":"Theorem Proving with the Real Numbers","author":"J Harrison","year":"2011","unstructured":"Harrison, J.: Theorem Proving with the Real Numbers, 1st edn. Springer, Berlin (2011)","edition":"1"},{"key":"9444_CR29","unstructured":"H\u00f6lzl, J.: Proving inequalities over reals with computation in Isabelle\/HOL. In: Proceedings of the ACM SIGSAM 2009 International Workshop on Programming Languages for Mechanized Mathematics Systems (PLMMS\u201909), Munich, pp. 38\u201345 (2009)"},{"key":"9444_CR30","doi-asserted-by":"crossref","unstructured":"H\u00f6lzl, J., Immler, F., Huffman, B.: Type classes and filters for mathematical analysis in Isabelle\/HOL. In: Interactive Theorem Proving (ITP 2013), volume 7998 of LNCS. Springer, pp. 279\u2013294 (2013)","DOI":"10.1007\/978-3-642-39634-2_21"},{"key":"9444_CR31","volume-title":"On the Direct Numerical Calculation of Elliptic Functions and Integrals","author":"LV King","year":"1924","unstructured":"King, L.V.: On the Direct Numerical Calculation of Elliptic Functions and Integrals. Cambridge University Press, Cambridge (1924)"},{"issue":"1","key":"9444_CR32","doi-asserted-by":"crossref","first-page":"1","DOI":"10.2168\/LMCS-9(1:1)2013","volume":"9","author":"R Krebbers","year":"2013","unstructured":"Krebbers, R., Spitters, B.: Type classes for efficient exact real arithmetic in Coq. Log. Methods Comput. Sci. 9(1), 1\u201327 (2013)","journal-title":"Log. Methods Comput. Sci."},{"issue":"7","key":"9444_CR33","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"issue":"3","key":"9444_CR34","doi-asserted-by":"crossref","first-page":"187","DOI":"10.1007\/s10817-015-9350-4","volume":"57","author":"\u00c9 Martin-Dorel","year":"2016","unstructured":"Martin-Dorel, \u00c9., Melquiond, G.: Proving tight bounds on univariate expressions with elementary functions in Coq. J. Autom. Reason. 57(3), 187\u2013217 (2016)","journal-title":"J. Autom. Reason."},{"key":"9444_CR35","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Wenzel, M., Paulson, L.C.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. Springer, Berlin (2002)"},{"key":"9444_CR36","doi-asserted-by":"crossref","unstructured":"O\u2019Connor, R.: Certified exact transcendental real number computation in Coq. In: Theorem Proving in Higher Order Logics: 21st International Conference, TPHOLs 2008, volume 5170 of LNCS. Springer, pp. 246\u2013261 (2008)","DOI":"10.1007\/978-3-540-71067-7_21"},{"issue":"135","key":"9444_CR37","first-page":"565","volume":"33","author":"E Salamin","year":"1976","unstructured":"Salamin, E.: Computation of $$\\pi $$ \u03c0 using arithmetic-geometric mean. Math. Comput. 33(135), 565\u2013570 (1976)","journal-title":"Math. Comput."},{"issue":"3\u20134","key":"9444_CR38","doi-asserted-by":"crossref","first-page":"281","DOI":"10.1007\/BF02242355","volume":"7","author":"A Sch\u00f6nhage","year":"1971","unstructured":"Sch\u00f6nhage, A., Strassen, V.: Schnelle Multiplikation gro\u00dfer Zahlen. Computing 7(3\u20134), 281\u2013292 (1971)","journal-title":"Computing"},{"key":"9444_CR39","doi-asserted-by":"crossref","unstructured":"Solovyev, A., Hales, T.C.: Formal verification of nonlinear inequalities with Taylor interval approximations. In: NASA Formal Methods: 5th International Symposium, NFM 2013, volume 7871 of LNCS. Springer, pp. 383\u2013397 (2013)","DOI":"10.1007\/978-3-642-38088-4_26"}],"container-title":["Journal of Automated Reasoning"],"original-title":[],"language":"en","link":[{"URL":"http:\/\/link.springer.com\/article\/10.1007\/s10817-017-9444-2\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9444-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/s10817-017-9444-2.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,10,8]],"date-time":"2019-10-08T05:03:01Z","timestamp":1570510981000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/s10817-017-9444-2"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2017,12,20]]},"references-count":39,"journal-issue":{"issue":"1-4","published-print":{"date-parts":[[2018,6]]}},"alternative-id":["9444"],"URL":"https:\/\/doi.org\/10.1007\/s10817-017-9444-2","relation":{},"ISSN":["0168-7433","1573-0670"],"issn-type":[{"type":"print","value":"0168-7433"},{"type":"electronic","value":"1573-0670"}],"subject":[],"published":{"date-parts":[[2017,12,20]]}}}