Skip to Main content Skip to Navigation
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.
Document type :
Conference papers
Complete list of metadata

Cited literature [20 references]  Display  Hide  Download
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 produced by the author(s)




Maxime Dénès, Anders Mörtberg, Vincent Siles. A refinement-based approach to computational algebra in COQ. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. pp.83-98, ⟨10.1007/978-3-642-32347-8_7⟩. ⟨hal-00734505⟩



Les métriques sont temporairement indisponibles