Haskell played a pivotal role in achieving this results. The Haskell kernel model described in our 2006 Haskell Workshop paper formed the basis for the verified high-performance C implementation and the kernel model used for verification — for details, see Klein et al.’s forthcoming SOSP paper.