{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,16]],"date-time":"2025-06-16T16:04:21Z","timestamp":1750089861960},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642323461"},{"type":"electronic","value":"9783642323478"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-32347-8_7","type":"book-chapter","created":{"date-parts":[[2012,8,10]],"date-time":"2012-08-10T11:33:54Z","timestamp":1344598434000},"page":"83-98","source":"Crossref","is-referenced-by-count":26,"title":["A Refinement-Based Approach to Computational Algebra in Coq"],"prefix":"10.1007","author":[{"given":"Maxime","family":"D\u00e9n\u00e8s","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Anders","family":"M\u00f6rtberg","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Vincent","family":"Siles","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"7_CR1","unstructured":"Abdeljaoued, J., Lombardi, H.: M\u00e9thodes matricielles - Introduction \u00e0 la complexit\u00e9 alg\u00e9brique. Springer (2004)"},{"key":"7_CR2","unstructured":"Barendregt, H., Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: The \u201cfundamental theorem of algebra\u201d project, \n                    \n                      http:\/\/www.cs.ru.nl\/~freek\/fta\/"},{"key":"7_CR3","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"86","DOI":"10.1007\/978-3-540-71067-7_11","volume-title":"Theorem Proving in Higher Order Logics","author":"Y. Bertot","year":"2008","unstructured":"Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical Big Operators. In: Mohamed, O.A., Mu\u00f1oz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol.\u00a05170, pp. 86\u2013101. Springer, Heidelberg (2008)"},{"issue":"3","key":"7_CR4","doi-asserted-by":"publisher","first-page":"251","DOI":"10.1016\/S0747-7171(08)80013-2","volume":"9","author":"D. Coppersmith","year":"1990","unstructured":"Coppersmith, D., Winograd, S.: Matrix multiplication via arithmetic progressions. Journal of Symbolic Computation\u00a09(3), 251\u2013280 (1990)","journal-title":"Journal of Symbolic Computation"},{"key":"7_CR5","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_CR6","unstructured":"Gonthier, G.: Formal proof\u2014the four-color theorem. In: Notices of the American Mathematical Society, vol.\u00a055, pp. 1382\u20131393 (2008)"},{"key":"7_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"103","DOI":"10.1007\/978-3-642-22863-6_10","volume-title":"Interactive Theorem Proving","author":"G. Gonthier","year":"2011","unstructured":"Gonthier, G.: Point-Free, Set-Free Concrete Linear Algebra. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol.\u00a06898, pp. 103\u2013118. Springer, Heidelberg (2011)"},{"key":"7_CR8","unstructured":"Gonthier, G., Mahboubi, A.: A Small Scale Reflection Extension for the COQ system. Technical report, Microsoft Research INRIA (2009), \n                    \n                      http:\/\/hal.inria.fr\/inria-00258384"},{"key":"7_CR9","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/11814771_36","volume-title":"Automated Reasoning","author":"B. Gr\u00e9goire","year":"2006","unstructured":"Gr\u00e9goire, B., Th\u00e9ry, L.: A Purely Functional Library for Modular Arithmetic and Its Application to Certifying Large Prime Numbers. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 423\u2013437. Springer, Heidelberg (2006)"},{"key":"7_CR10","doi-asserted-by":"crossref","unstructured":"Hales, T.C.: The jordan curve theorem, formally and informally. In: The American Mathematical Monthly, vol.\u00a0114, pp. 882\u2013894 (2007)","DOI":"10.1080\/00029890.2007.11920481"},{"key":"7_CR11","unstructured":"Karatsuba, A., Ofman, Y.: Multiplication of many-digital numbers by automatic computers. In: USSR Academy of Sciences, vol.\u00a0145, pp. 293\u2013294 (1962)"},{"key":"7_CR12","unstructured":"Knuth, D.E.: The art of computer programming, vol.2: seminumerical algorithms. Addison-Wesley (1981)"},{"key":"7_CR13","series-title":"Lecture Notes in Artificial Intelligence","doi-asserted-by":"publisher","first-page":"438","DOI":"10.1007\/11814771_37","volume-title":"Automated Reasoning","author":"A. Mahboubi","year":"2006","unstructured":"Mahboubi, A.: Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol.\u00a04130, pp. 438\u2013452. Springer, Heidelberg (2006)"},{"key":"7_CR14","doi-asserted-by":"crossref","unstructured":"Mines, R., Richman, F., Ruitenburg, W.: A Course in Constructive Algebra. Springer (1988)","DOI":"10.1007\/978-1-4419-8640-5"},{"key":"7_CR15","unstructured":"O\u2019Connor, R.: Karatsuba\u2019s multiplication, \n                    \n                      http:\/\/coq.inria.fr\/V8.2pl1\/contribs\/Karatsuba.html"},{"key":"7_CR16","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)"},{"key":"7_CR17","unstructured":"Palomo-Lozano, F., Medina-Bulo, I., Alonso-Jim\u00e9nez, J.: Certification of matrix multiplication algorithms. strassen\u2019s algorithm in ACL2. In: Supplemental Proceedings of the 14th International Conference on Theorem Proving in Higher Order Logics, Informatics Research Report EDI-INF-RR-0046, Edinburgh (2001)"},{"key":"7_CR18","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)"},{"issue":"4","key":"7_CR19","doi-asserted-by":"publisher","first-page":"354","DOI":"10.1007\/BF02165411","volume":"13","author":"V. Strassen","year":"1969","unstructured":"Strassen, V.: Gaussian elimination is not optimal. Numerische Mathematik\u00a013(4), 354\u2013356 (1969)","journal-title":"Numerische Mathematik"},{"key":"7_CR20","doi-asserted-by":"publisher","first-page":"381","DOI":"10.1016\/0024-3795(71)90009-7","volume":"4","author":"S. Winograd","year":"1971","unstructured":"Winograd, S.: On multiplication of 2x2 matrices. Linear Algebra and its Applications\u00a04, 381\u2013388 (1971)","journal-title":"Linear Algebra and its Applications"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-32347-8_7.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,5,4]],"date-time":"2021-05-04T12:01:13Z","timestamp":1620129673000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-32347-8_7"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642323461","9783642323478"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-32347-8_7","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}