Tabulation hashing was first introduced under the name of Zobrist-hashing where it was used for highly efficient look-up tables for chess positions.
Later it was discovered that it forms a 3-independent hash family. This means that when values of the hash function on any three domain elements form independent and uniformly distributed random variables. Such properties can then be used for the verification of randomized alogorithms. (A simple example would be a hash table.)
The aim of this project is to construct a scheme for tabulation based hashing and verify that it fullfils the corresponding properties defined in the AFP library. It is possible to extend the scope of the project, for example by including schemes for hashing variable length strings.
- Basic familiarity with probability theory (espically independence of random variables) is useful.
- Experience with Isabelle/HOL is required.