{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,6]],"date-time":"2024-09-06T04:04:09Z","timestamp":1725595449885},"publisher-location":"Berlin, Heidelberg","reference-count":36,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642226724"},{"type":"electronic","value":"9783642226731"}],"license":[{"start":{"date-parts":[[2011,1,1]],"date-time":"2011-01-01T00:00:00Z","timestamp":1293840000000},"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":[[2011]]},"DOI":"10.1007\/978-3-642-22673-1_7","type":"book-chapter","created":{"date-parts":[[2011,7,13]],"date-time":"2011-07-13T07:49:15Z","timestamp":1310543355000},"page":"90-106","source":"Crossref","is-referenced-by-count":7,"title":["Computer Certified Efficient Exact Reals in Coq"],"prefix":"10.1007","author":[{"given":"Robbert","family":"Krebbers","sequence":"first","affiliation":[]},{"given":"Bas","family":"Spitters","sequence":"additional","affiliation":[]}],"member":"297","reference":[{"key":"7_CR1","volume-title":"Foundations of constructive analysis","author":"E.A. Bishop","year":"1967","unstructured":"Bishop, E.A.: Foundations of constructive analysis. McGraw-Hill, New York (1967)"},{"issue":"1","key":"7_CR2","first-page":"129","volume":"17","author":"R. O\u2019Connor","year":"2007","unstructured":"O\u2019Connor, R.: A Monadic, Functional Implementation of Real Numbers. MSCS\u00a017(1), 129\u2013159 (2007)","journal-title":"MSCS"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"246","DOI":"10.1007\/978-3-540-71067-7_21","volume-title":"Theorem Proving in Higher Order Logics","author":"R. O\u2019Connor","year":"2008","unstructured":"O\u2019Connor, R.: Certified Exact Transcendental Real Number Computation in Coq. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 246\u2013261. Springer, Heidelberg (2008)"},{"issue":"37","key":"7_CR4","doi-asserted-by":"publisher","first-page":"3386","DOI":"10.1016\/j.tcs.2010.05.031","volume":"411","author":"R. O\u2019Connor","year":"2010","unstructured":"O\u2019Connor, R., Spitters, B.: A computer verified, monadic, functional implementation of the integral. TCS\u00a0411(37), 3386\u20133402 (2010)","journal-title":"TCS"},{"issue":"2-3","key":"7_CR5","doi-asserted-by":"publisher","first-page":"95","DOI":"10.1016\/0890-5401(88)90005-3","volume":"76","author":"T. Coquand","year":"1988","unstructured":"Coquand, T., Huet, G.: The Calculus of Constructions. Information and Computation\u00a076(2-3), 95\u2013120 (1988)","journal-title":"Information and Computation"},{"key":"7_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"50","DOI":"10.1007\/3-540-52335-9_47","volume-title":"COLOG-88","author":"T. Coquand","year":"1990","unstructured":"Coquand, T., Paulin, C.: Inductively defined types. In: Martin-L\u00f6f, P., Mints, G. (eds.) COLOG 1988. LNCS, vol.\u00a0417, pp. 50\u201366. Springer, Heidelberg (1990)"},{"key":"7_CR7","unstructured":"Coq Development Team: The Coq Proof Assistant Reference Manual. INRIA-Rocquencourt (2008)"},{"key":"7_CR8","series-title":"Texts in TCS","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5","volume-title":"Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions","author":"Y. Bertot","year":"2004","unstructured":"Bertot, Y., Cast\u00e9ran, P.: Interactive Theorem Proving and Program Development. Coq\u2019Art: The Calculus of Inductive Constructions. Texts in TCS. Springer, Heidelberg (2004)"},{"key":"7_CR9","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: An intuitionistic theory of types. In: Twenty-five years of constructive type theory. Oxford Logic Guides, vol.\u00a036, pp. 127\u2013172. OUP (1998)","DOI":"10.1093\/oso\/9780198501275.003.0010"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Martin-L\u00f6f, P.: Constructive Mathematics and Computer Science. In: Logic, Methodology and the Philosophy of Science VI. Studies in Logic and the Foundations of Mathematics, vol.\u00a0104, pp. 153\u2013175 (1982)","DOI":"10.1016\/S0049-237X(09)70189-2"},{"key":"7_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"359","DOI":"10.1007\/978-3-540-69407-6_39","volume-title":"Logic and Theory of Algorithms","author":"P. Letouzey","year":"2008","unstructured":"Letouzey, P.: Extraction in Coq: An Overview. In: Beckmann, A., Dimitracopoulos, C., L\u00f6we, B. (eds.) CiE 2008. LNCS, vol.\u00a05028, pp. 359\u2013369. Springer, Heidelberg (2008)"},{"key":"7_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"205","DOI":"10.1007\/10930755_14","volume-title":"Theorem Proving in Higher Order Logics","author":"L. Cruz-Filipe","year":"2003","unstructured":"Cruz-Filipe, L., Spitters, B.: Program Extraction from Large Proof Developments. In: Basin, D., Wolff, B. (eds.) TPHOLs 2003. LNCS, vol.\u00a02758, pp. 205\u2013220. Springer, Heidelberg (2003)"},{"issue":"1","key":"7_CR13","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.entcs.2005.11.024","volume":"151","author":"L. Cruz-Filipe","year":"2006","unstructured":"Cruz-Filipe, L., Letouzey, P.: A Large-Scale Experiment in Executing Extracted Programs. Electronic Notes in Theoretical Computer Science\u00a0151(1), 75\u201391 (2006)","journal-title":"Electronic Notes in Theoretical Computer Science"},{"key":"7_CR14","series-title":"CPHC\/BCS Distinguished Dissertations","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4471-0963-1","volume-title":"Extensional constructs in intensional type theory","author":"M. Hofmann","year":"1997","unstructured":"Hofmann, M.: Extensional constructs in intensional type theory. CPHC\/BCS Distinguished Dissertations. Springer, Heidelberg (1997)"},{"key":"7_CR15","unstructured":"Palmgren, E.: Constructivist and Structuralist Foundations: Bishops and Lawveres Theories of Sets. Technical Report\u00a04, Mittag-Leffler (2009)"},{"issue":"1","key":"7_CR16","first-page":"41","volume":"2","author":"M. Sozeau","year":"2009","unstructured":"Sozeau, M.: A New Look at Generalized Rewriting in Type Theory. Journal of Formalized Reasoning\u00a02(1), 41\u201362 (2009)","journal-title":"Journal of Formalized Reasoning"},{"key":"7_CR17","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"278","DOI":"10.1007\/978-3-540-71067-7_23","volume-title":"Theorem Proving in Higher Order Logics","author":"M. Sozeau","year":"2008","unstructured":"Sozeau, M., Oury, N.: First-class type classes. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 278\u2013293. Springer, Heidelberg (2008)"},{"key":"7_CR18","doi-asserted-by":"crossref","unstructured":"Spitters, B., van der Weegen, E.: Type classes for mathematics in type theory. MSCS, special issue on Interactive theorem proving and the formalization of mathematics (2011)","DOI":"10.1017\/S0960129511000119"},{"key":"7_CR19","doi-asserted-by":"crossref","unstructured":"Gr\u00e9goire, B., Leroy, X.: A compiled implementation of strong reduction. In: ICFP, pp. 235\u2013246 (2002)","DOI":"10.1145\/583852.581501"},{"key":"7_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"83","DOI":"10.1007\/978-3-642-14052-5_8","volume-title":"Interactive Theorem Proving","author":"M. Armand","year":"2010","unstructured":"Armand, M., Gr\u00e9goire, B., Spiwack, A., Th\u00e9ry, L.: Extending Coq with imperative features and its application to SAT verification. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol.\u00a06172, pp. 83\u201398. Springer, Heidelberg (2010)"},{"key":"7_CR21","unstructured":"Spiwack, A.: Verified Computing in Homological Algebra, A Journey Exploring the Power and Limits of Dependent Type Theory. PhD thesis, INRIA (2011)"},{"issue":"1","key":"7_CR22","doi-asserted-by":"publisher","first-page":"98","DOI":"10.1002\/malq.200710024","volume":"54","author":"F. Richman","year":"2008","unstructured":"Richman, F.: Real numbers and other completions. Mathematical Logic Quarterly\u00a054(1), 98\u2013108 (2008)","journal-title":"Mathematical Logic Quarterly"},{"key":"7_CR23","doi-asserted-by":"crossref","unstructured":"Moggi, E.: Computational lambda-calculus and monads. In: LICS, pp. 14\u201323 (1989)","DOI":"10.1109\/LICS.1989.39155"},{"key":"7_CR24","doi-asserted-by":"crossref","unstructured":"Wadler, P.: Monads for functional programming. In: Proceedings of the Marktoberdorf Summer School on Program Design Calculi (August 1992)","DOI":"10.1007\/978-3-662-02880-3_8"},{"key":"7_CR25","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"327","DOI":"10.1007\/978-3-642-03359-9_23","volume-title":"Theorem Proving in Higher Order Logics","author":"F. Garillot","year":"2009","unstructured":"Garillot, F., Gonthier, G., Mahboubi, A., Rideau, L.: Packaging mathematical structures. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 327\u2013342. Springer, Heidelberg (2009)"},{"key":"7_CR26","unstructured":"Gonthier, G., Mahboubi, A., Tassi, E.: A Small Scale Reflection Extension for the Coq system. Technical Report RR-6455, INRIA (2008)"},{"issue":"3","key":"7_CR27","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/j.apal.2008.09.025","volume":"159","author":"A. Bauer","year":"2009","unstructured":"Bauer, A., Kavkler, I.: A constructive theory of continuous domains suitable for implementation. Annals of Pure and Applied Logic\u00a0159(3), 251\u2013267 (2009)","journal-title":"Annals of Pure and Applied Logic"},{"key":"7_CR28","unstructured":"O\u2019Connor, R.: Incompleteness and Completeness: Formalizing Logic and Analysis in Type Theory. PhD thesis, Radboud University Nijmegen (2009)"},{"key":"7_CR29","doi-asserted-by":"crossref","unstructured":"Wolfram, S.: A new kind of science. Wolfram Media (2002)","DOI":"10.1115\/1.1553433"},{"key":"7_CR30","doi-asserted-by":"crossref","unstructured":"Gonthier, G., Ziliani, B., Nanevski, A., Dreyer, D.: Making ad hoc proof automation less ad hoc (2011)","DOI":"10.1145\/2034773.2034798"},{"key":"7_CR31","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"84","DOI":"10.1007\/978-3-642-03359-9_8","volume-title":"Theorem Proving in Higher Order Logics","author":"A. Asperti","year":"2009","unstructured":"Asperti, A., Ricciotti, W., Coen, C., Tassi, E.: Hints in Unification. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 84\u201398. Springer, Heidelberg (2009)"},{"key":"7_CR32","doi-asserted-by":"crossref","unstructured":"Boldo, S., Melquiond, G.: Flocq: A unified library for proving floating-point algorithms in Coq. In: Proc 20th IEEE Symposium on Computer Arithmetic (2011)","DOI":"10.1109\/ARITH.2011.40"},{"key":"7_CR33","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"408","DOI":"10.1007\/978-3-642-03359-9_28","volume-title":"Theorem Proving in Higher Order Logics","author":"N. Julien","year":"2009","unstructured":"Julien, N., Pasca, I.: Formal Verification of Exact Computations Using Newton\u2019s Method. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds.) TPHOLs 2009. LNCS, vol.\u00a05674, pp. 408\u2013423. Springer, Heidelberg (2009)"},{"issue":"1","key":"7_CR34","first-page":"37","volume":"17","author":"Y. Bertot","year":"2007","unstructured":"Bertot, Y.: Affine functions and series with co-inductive real numbers. MSCS\u00a017(1), 37\u201363 (2007)","journal-title":"MSCS"},{"key":"7_CR35","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"48","DOI":"10.1007\/978-3-540-78969-7_6","volume-title":"Functional and Logic Programming","author":"N. Julien","year":"2008","unstructured":"Julien, N.: Certified Exact Real Arithmetic Using Co-induction in Arbitrary Integer Base. In: Garrigue, J., Hermenegildo, M.V. (eds.) FLOPS 2008. LNCS, vol.\u00a04989, pp. 48\u201363. Springer, Heidelberg (2008)"},{"key":"7_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"132","DOI":"10.1007\/978-3-642-04027-6_12","volume-title":"Computer Science Logic","author":"U. Berger","year":"2009","unstructured":"Berger, U.: From coinductive proofs to exact real arithmetic. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol.\u00a05771, pp. 132\u2013146. Springer, Heidelberg (2009)"}],"container-title":["Lecture Notes in Computer Science","Intelligent Computer Mathematics"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-22673-1_7","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,11,27]],"date-time":"2021-11-27T19:36:47Z","timestamp":1638041807000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-22673-1_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011]]},"ISBN":["9783642226724","9783642226731"],"references-count":36,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-22673-1_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2011]]}}}