This code was primarily written by Jonathan Protzenko and Cédric Fournet (MSR).
An earlier version was written by Benjamin Beurdouche (INRIA).