Robbert Krebbers

About

Robbert I am a post-doc, supervised by Lars Birkedal, in the Logic and Semantics group of Aarhus University. I am working on program logics for concurrency.

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.

News

On December 1, 2015 at Radboud University Nijmegen, I have defended by PhD thesis entitled The C standard formalized in Coq. I am honored to have received a cum laude distinction.

The day following my defense, we have organized a workshop called Workshop on Realistic Program Verification at the Radboud University Nijmegen.

Software

Contact

(λ x y . mail @ x y . nl) robbert krebbers

Address

Snail mail: Department of Computer Science, Åbogade 34, 8200 Aarhus N, Denmark
Office: building 5341 (Turing), office 215, Åbogade 34, Denmark