Robbert Krebbers

I am a PhD student, supervised by Freek Wiedijk and Herman Geuvers, in the Foundations Group of the Radboud University Nijmegen. I am working on a formal operational and axiomatic semantics covering interesting features of the C11 standard. These features include: non-local control (goto, return, break, continue), 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 am using the proof assistant Coq. The most recent version of the Coq development is available 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. Apart from that, I have strong interests in type theory, and computational content of classical logic.

Publications

2014

2013

2012

2011

2010

Talks

The list below contains some slides of talks that do not have a corresponding conference paper. Slides corresponding to my conference papers can be found in the list above.

Software

Contact

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