A refinement-based approach to computational algebra in COQ - Archive ouverte HAL Access content directly
Conference Papers Year : 2012

A refinement-based approach to computational algebra in COQ

(1) , (2) , (2)
1
2

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.
Fichier principal
Vignette du fichier
coqeal.pdf (133.31 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

hal-00734505 , version 1 (22-09-2012)

Identifiers

Cite

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⟩

Collections

INRIA INRIA2
315 View
462 Download

Altmetric

Share

Gmail Facebook Twitter LinkedIn More