From Sets to Bits in Coq
| Autor: | Julia Lawall, Arthur Blot, Pierre-Évariste Dagand |
|---|---|
| Přispěvatelé: | Well Honed Infrastructure Software for Programming Environments and Runtimes ( Whisper), Laboratoire d'Informatique de Paris 6 (LIP6), Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Université Pierre et Marie Curie - Paris 6 (UPMC)-Centre National de la Recherche Scientifique (CNRS)-Inria de Paris, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Blot, Arthur |
| Rok vydání: | 2016 |
| Předmět: |
[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO]
Theoretical computer science Computer science Programming language business.industry Computer programming Proof assistant [INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] 020207 software engineering 02 engineering and technology Bloom filter ENCODE Symbolic computation computer.software_genre Development (topology) 020204 information systems 0202 electrical engineering electronic engineering information engineering Memory footprint business computer Finite set |
| Zdroj: | Functional and Logic Programming ISBN: 9783319296036 FLOPS FLOPS 2016 FLOPS 2016, Mar 2016, Kochi, Japan |
| Popis: | International audience; 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|