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.

Together with Josef Urban, I am organizing the weekly Brouwer seminar of the Foundations Group. If you wish to give a talk, please contact me.

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