In this talk, I describe the specification and proof of an (imperative, sequential) hash table implementation. The usual dictionary operations (insertion, lookup, and so on) are supported, as well as iteration via folds and iterators. The code is written in OCaml and verified using higher-order separation logic, embedded in Coq, via the CFML tool and library. This case study is part of ANR project Vocal, whose aim is to build a verified OCaml library of basic data structures.

(This work was presented at CPP 2017.)