Abstract
We describe a step-by-step approach to the implementation and formal verification of efficient algebraic algorithms. Formal specifications are expressed on rich data types which are suitable for deriving essential theoretical properties. These specifications are then refined to concrete implementations on more efficient data structures and linked to their abstract counterparts. We illustrate this methodology on key applications: matrix rank computation, Winograd’s fast matrix product, Karatsuba’s polynomial multiplication, and the gcd of multivariate polynomials.
The research leading to these results has received funding from the European Union’s 7th Framework Programme under grant agreement nr. 243847 (ForMath).
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abdeljaoued, J., Lombardi, H.: Méthodes matricielles - Introduction à la complexité algébrique. Springer (2004)
Barendregt, H., Geuvers, H., Pollack, R., Wiedijk, F., Zwanenburg, J.: The “fundamental theorem of algebra” project, http://www.cs.ru.nl/~freek/fta/
Bertot, Y., Gonthier, G., Ould Biha, S., Pasca, I.: Canonical Big Operators. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 86–101. Springer, Heidelberg (2008)
Coppersmith, D., Winograd, S.: Matrix multiplication via arithmetic progressions. Journal of Symbolic Computation 9(3), 251–280 (1990)
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. 5674, pp. 327–342. Springer, Heidelberg (2009)
Gonthier, G.: Formal proof—the four-color theorem. In: Notices of the American Mathematical Society, vol. 55, pp. 1382–1393 (2008)
Gonthier, G.: Point-Free, Set-Free Concrete Linear Algebra. In: van Eekelen, M., Geuvers, H., Schmaltz, J., Wiedijk, F. (eds.) ITP 2011. LNCS, vol. 6898, pp. 103–118. Springer, Heidelberg (2011)
Gonthier, G., Mahboubi, A.: A Small Scale Reflection Extension for the COQ system. Technical report, Microsoft Research INRIA (2009), http://hal.inria.fr/inria-00258384
Grégoire, B., Théry, 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. 4130, pp. 423–437. Springer, Heidelberg (2006)
Hales, T.C.: The jordan curve theorem, formally and informally. In: The American Mathematical Monthly, vol. 114, pp. 882–894 (2007)
Karatsuba, A., Ofman, Y.: Multiplication of many-digital numbers by automatic computers. In: USSR Academy of Sciences, vol. 145, pp. 293–294 (1962)
Knuth, D.E.: The art of computer programming, vol.2: seminumerical algorithms. Addison-Wesley (1981)
Mahboubi, A.: Proving Formally the Implementation of an Efficient gcd Algorithm for Polynomials. In: Furbach, U., Shankar, N. (eds.) IJCAR 2006. LNCS (LNAI), vol. 4130, pp. 438–452. Springer, Heidelberg (2006)
Mines, R., Richman, F., Ruitenburg, W.: A Course in Constructive Algebra. Springer (1988)
O’Connor, R.: Karatsuba’s multiplication, http://coq.inria.fr/V8.2pl1/contribs/Karatsuba.html
O’Connor, R.: Certified Exact Transcendental Real Number Computation in COQ. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 246–261. Springer, Heidelberg (2008)
Palomo-Lozano, F., Medina-Bulo, I., Alonso-Jiménez, J.: Certification of matrix multiplication algorithms. strassen’s 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)
Sozeau, M., Oury, N.: First-Class Type Classes. In: Mohamed, O.A., Muñoz, C., Tahar, S. (eds.) TPHOLs 2008. LNCS, vol. 5170, pp. 278–293. Springer, Heidelberg (2008)
Strassen, V.: Gaussian elimination is not optimal. Numerische Mathematik 13(4), 354–356 (1969)
Winograd, S.: On multiplication of 2x2 matrices. Linear Algebra and its Applications 4, 381–388 (1971)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Dénès, M., Mörtberg, A., Siles, V. (2012). A Refinement-Based Approach to Computational Algebra in Coq . In: Beringer, L., Felty, A. (eds) Interactive Theorem Proving. ITP 2012. Lecture Notes in Computer Science, vol 7406. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-32347-8_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-32347-8_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-32346-1
Online ISBN: 978-3-642-32347-8
eBook Packages: Computer ScienceComputer Science (R0)