Refinements for Free!

Abstract : Formal verification of algorithms often requires a choice be-tween definitions that are easy to reason about and definitions that are computationally efficient. One way to reconcile both consists in adopt-ing a high-level view when proving correctness and then refining stepwise down to an efficient low-level implementation. Some refinement steps are interesting, in the sense that they improve the algorithms involved, while others only express a switch from data representations geared towards proofs to more efficient ones geared towards computations. We relieve the user of these tedious refinements by introducing a framework where correctness is established in a proof-oriented context and automatically transported to computation-oriented data structures. Our design is gen-eral enough to encompass a variety of mathematical objects, such as rational numbers, polynomials and matrices over refinable structures. Moreover, the rich formalism of the Coq proof assistant enables us to develop this within Coq, without having to maintain an external tool.
Type de document :
Communication dans un congrès
Certified Programs and Proofs, Dec 2013, Melbourne, Australia. pp.147 - 162, 2013, <10.1007/978-3-319-03545-1_10>


https://hal.inria.fr/hal-01113453
Contributeur : Cyril Cohen <>
Soumis le : jeudi 5 février 2015 - 14:52:18
Dernière modification le : mercredi 14 décembre 2016 - 01:06:48
Document(s) archivé(s) le : mercredi 6 mai 2015 - 10:21:25

Fichier

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

Identifiants

Collections

Citation

Cyril Cohen, Maxime Dénès, Anders Mörtberg. Refinements for Free!. Certified Programs and Proofs, Dec 2013, Melbourne, Australia. pp.147 - 162, 2013, <10.1007/978-3-319-03545-1_10>. <hal-01113453>

Partager

Métriques

Consultations de
la notice

206

Téléchargements du document

141