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.
Type de document :
Communication dans un congrès
Lennart Beringer and Amy Felty. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. Springer, 7406, pp.83-98, 2012, Lecture Notes In Computer Science. 〈10.1007/978-3-642-32347-8_7〉
Liste complète des métadonnées

Littérature citée [20 références]  Voir  Masquer  Télécharger
https://hal.inria.fr/hal-00734505
Contributeur : Maxime Dénès <>
Soumis le : samedi 22 septembre 2012 - 16:10:22
Dernière modification le : jeudi 11 janvier 2018 - 16:21:52
Document(s) archivé(s) le : dimanche 23 décembre 2012 - 03:00:10

Fichiers

coqeal.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

Collections

INRIA | UNIV-COTEDAZUR

Citation

Maxime Dénès, Anders Mörtberg, Vincent Siles. A refinement-based approach to computational algebra in COQ. Lennart Beringer and Amy Felty. ITP - 3rd International Conference on Interactive Theorem Proving - 2012, Aug 2012, Princeton, United States. Springer, 7406, pp.83-98, 2012, Lecture Notes In Computer Science. 〈10.1007/978-3-642-32347-8_7〉. 〈hal-00734505〉

Exporter

BibTeX TEI DC DCterms EndNote

Partager

Métriques

Consultations de la notice

502

Téléchargements de fichiers

333

Contact


archive-ouverte@inria.fr