From Sets to Bits in Coq

Abstract : Computer Science abounds in folktales about how — in the early days of computer programming — bit vectors were ingeniously used to encode and manipulate finite sets. Algorithms have thus been developed to minimize memory footprint and maximize efficiency by taking advantage of microarchitectural features. With the development of automated and interactive theorem provers, finite sets have also made their way into the libraries of formalized mathematics. Tailored to ease proving , these representations are designed for symbolic manipulation rather than computational efficiency. This paper aims to bridge this gap. In the Coq proof assistant, we implement a bitset library and prove its correct-ness with respect to a formalization of finite sets. Our library enables a seamless interaction of sets for computing — bitsets — and sets for proving — finite sets.
Type de document :
Communication dans un congrès
FLOPS 2016, Mar 2016, Kochi, Japan
Liste complète des métadonnées


https://hal.archives-ouvertes.fr/hal-01251943
Contributeur : Arthur Blot <>
Soumis le : jeudi 7 janvier 2016 - 06:04:35
Dernière modification le : mercredi 20 juillet 2016 - 11:44:52
Document(s) archivé(s) le : vendredi 8 avril 2016 - 13:08:57

Fichier

flops-blot-dagand-lawall.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : hal-01251943, version 1

Collections

Citation

Arthur Blot, Pierre-Évariste Dagand, Julia Lawall. From Sets to Bits in Coq. FLOPS 2016, Mar 2016, Kochi, Japan. <hal-01251943>

Partager

Métriques

Consultations de
la notice

281

Téléchargements du document

117