Hash tables are a very common data structure. One application of hash tables is hash- consing, which is used in particular for extensions of the CompCert verified compiler.
Hash tables are fundamentally an imperative structure, based on arrays. Coq used not to support arrays natively, and thus Coq programs using hash-consing had to be implemented using various tricks (calls to OCaml code through smart constructors, etc.). These tricks enlarge the trusted computing base.
Arrays have since then been added to Coq as native datatypes. The purpose of the internship is to build a verified hashtable and possibly hash-consing library.
