I am a PhD student in the Foundations Group of the Radboud University Nijmegen. Together with Freek Wiedijk, I am working on a mathemically precise version of the C99 standard in the proof assistants HOL, Isabelle and Coq. More information about this project can be found here.
Previously, I have been working with Bas Spitters on a fast implementation of the real numbers in the proof assistant Coq. Our implementation, which is based on a previous implementation by Russell O’Connor, makes heavy use of Coq's new type classes and support for machine integers.
(λ x y . mail @ x y . nl) robbert krebbers