Sciweavers

Share
FLOPS
2016
Springer

From Sets to Bits in Coq

4 years 3 months ago
From Sets to Bits in Coq
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 correctness 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.
Arthur Blot, Pierre-Évariste Dagand, Julia
Added 03 Apr 2016
Updated 03 Apr 2016
Type Journal
Year 2016
Where FLOPS
Authors Arthur Blot, Pierre-Évariste Dagand, Julia Lawall
Comments (0)
books