| HAL-Inria | Publications, software ... of Inria's scientists |
Conference papers
A refinement-based approach to computational algebra in COQ
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.
Cited literature [20 references]
https://hal.inria.fr/hal-00734505
Contributor : Maxime Dénès Connect in order to contact the contributor
Submitted on : Saturday, September 22, 2012 - 4:10:22 PM
Last modification on : Thursday, January 7, 2021 - 3:40:05 PM
Long-term archiving on: : Sunday, December 23, 2012 - 3:00:10 AM
Contributor : Maxime Dénès Connect in order to contact the contributor
Submitted on : Saturday, September 22, 2012 - 4:10:22 PM
Last modification on : Thursday, January 7, 2021 - 3:40:05 PM
Long-term archiving on: : Sunday, December 23, 2012 - 3:00:10 AM
Files
coqeal.pdf
Files produced by the author(s)