A refinement-based approach to computational algebra in COQ

Maxime Dénès 1 Anders Mörtberg 2 Vincent Siles 2
1 MARELLE - Mathematical, Reasoning and Software
CRISAM - Inria Sophia Antipolis - Méditerranée
2 CSE - Department of Computer Science and Engineering [Göteborg]
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 metadatas

Cited literature [20 references]  Display  Hide  Download
https://hal.inria.fr/hal-00734505
Contributor : Maxime Dénès <>
Submitted on : Saturday, September 22, 2012 - 4:10:22 PM
Last modification on : Thursday, January 11, 2018 - 4:21:52 PM
Long-term archiving on : Sunday, December 23, 2012 - 3:00:10 AM

Files

coqeal.pdf
Files produced by the author(s)

Identifiers

Collections

INRIA | UNIV-COTEDAZUR

Citation

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⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

600

Files downloads

433

Contact


archive-ouverte@inria.fr