Sites Inria

English version

Séminaire des équipes de recherche

From Sets to Bits in Coq

© INRIA Sophie Auvin - G comme Grille

  • Date : 9/05/2016
  • Lieu : 2 rue Simone Iff, 75012 Paris (ou: 41 rue du Charolais) - Salle Jacques-Louis Lions 1, bâtiment C
  • Intervenant(s) : Pierre-Évariste Dagand, Sorbonne Université, CNRS, Inria, LIP6

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. In this talk, we shall bridge this gap and present a Coq library that enables a seamless interaction of sets for computing - bitsets - and sets for proving - finite sets.
This is joint work with Arthur Blot and Julia Lawall.

Mots-clés : Event Memory Gallium Structures Models Weak

Haut de page

Suivez Inria