Structures de données à la Caml pour Coq:
L'exemple des ensembles finis et des tables d'association


Dans cet exposé, je présenterai les efforts d'adaptation à Coq des
bibliothèques Ocaml de structures de données Set et Map. Ce travail a
pour double objectif de garantir à l'utilisateur d'Ocaml la correction
de ces librairies Set et Map, et d'autre part de fournir à
l'utilisateur de Coq des structures plus riches et efficaces que de
simples listes. Même si la partie concernant Set a été réalisé avec
Jean-Christophe Filliâtre il y a bientôt trois ans, l'extension
récente à Map avec Pierre Courtieu a donné lieu à une refonte en
profondeur de cette bibliothèque Coq, avec en point de mire
l'inclusion prochaine dans les théories standards de Coq. Je tenterai
donc de décrire les points clés de ces travaux, tels que:
- l'usage des modules Coq pour spécifier et prouver du logiciel
- les différentes manières de programmer en Coq
- les possibilités de calcul associées, que ce soit en interne
(machine virtuelle) ou en externe (extraction)