This code was primarily written by Marina Polubelova (INRIA).
Jonathan Protzenko contributed the design of the type classes hierarchy.