Before that, I was a PhD student, supervised by Freek Wiedijk and Herman Geuvers, in the Foundations Group of the Radboud University Nijmegen. As part of my PhD thesis I have developed an operational, executable and axiomatic semantics of the C programming language. My semantics is based on the description of C by the C11 standard, and can therefore be used to reason about C programs in a compiler independent way. It covers delicate features of C such as non-local control (goto, return, break, continue and unstructured switch), non-determistic expression evaluation with sequence points, a defect report #260 compliant memory model (supporting C11's strong aliassing restrictions). For the development of this semantics, I have used the proof assistant Coq. The most recent version of the Coq development is available here.
I have also 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.
Apart from that, I have strong interests in type theory, and computational content of classical logic.
I will defend my PhD thesis entitled The C standard formalized in Coq on Tuesday December 1, 2015 at 10.30. The defense will take place in the Auditorium (Aula) of the Radboud University Nijmegen, Comeniuslaan 2, 6525 HP in Nijmegen.
The day after my defense, Wednesday December 2, there will be a workshop called Workshop on Realistic Program Verification at the Radboud University Nijmegen.
- My GitHub repository
- CH2O: A formalization of the C11 standard in Coq
- C-CORN: Coq Repository at Nijmegen
- Math classes
(λ x y . mail @ x y . nl) robbert krebbers
Snail mail: Department of Computer Science, Åbogade 34, 8200 Aarhus N, Denmark
Office: building 5341 (Turing), office 215, Åbogade 34, Denmark