Vous pouvez vous abonner à nos annonces de séminaires
http://gallium.inria.fr/seminaires/
S E M I N A I R E
__
/ _` _ / / o
/ ) __) / / / / / /\/|
(___/ (_/ (_ (_ / (__/ / |
I N R I A - Paris
2 rue Simone Iff (ou: 41 rue du Charolais)
Salle Lions 1, bâtiment C
Lundi 9 mai, 10h30
----------------------
Pierre-Évariste Dagand
----------------------
Sorbonne Universités, CNRS, Inria, LIP6
========================
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. 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.