Bachelor Thesis
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.)
Since then more advance tabulation based solutions have also been found. See for example Thorup and Zhang or Lemire.
There already is an AFP entry for univeral hash families, which includes a formulation of the more flexible (but computationally more expensive) Carter-Wegman hash family.
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.
Prerequisites:
- Basic familiarity with probability theory (espically independence of random variables) is useful.
- Experience with Isabelle/HOL is required.
Professor:
Tobias Nipkow
Advisors:
Emin Karayel
Yong Kiam Tan