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.
- Robbert Krebbers.
Aliasing restrictions of C11 formalized in Coq.
In CPP, volume 8307 of LNCS, pages 50-65.
- Robbert Krebbers and Freek Wiedijk.
Separation Logic for Non-local Control Flow and Block Scope Variables.
In FoSSaCS, volume 7794 of LNCS, pages 257-272.
Awarded best student contribution.
- Herman Geuvers, Robbert Krebbers and James McKinna.
In volume 164, issue 6 of APAL, pages 676–701.
- Robbert Krebbers and Bas Spitters.
Type classes for efficient exact real arithmetic in Coq.
In volume 9, issue 1, of LMCS, pages 1-27.
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.
- Moessner's Theorem: an exercise in coinductive reasoning in Coq.
At the COIN seminar, November 12, 2013, CWI, Amsterdam, the Netherlands.
- Separation Logic for Non-local Control Flow and Block Scope Variables.
At the Gallium seminar, February 4, 2013, INRIA Rocquencourt, Paris, France.
- Separation Logic for Non-local Control Flow.
At the Brouwer seminar, November 20, 2012, Radboud University, Nijmegen, the Netherlands.
- Formalizing the C99 standard (invited talk).
At ICT.OPEN, November 15, 2011, Veldhoven, the Netherlands.
- Type Classes for Efficient Exact Real Arithmetic in Coq.
At TYPES, September 9, 2011, Bergen, Norway.
- Computer certified efficient exact reals in Coq
At the the Coq Workshop, August 26, 2011, Nijmegen, the Netherlands.
- Computer certified efficient exact reals in Coq.
At the Brouwer seminar, March 22, 2011, Radboud University, Nijmegen, the Netherlands.
- Type Classes for Mathematics.
At the Workshop on reification and generic tactics, March 31, 2011, INRIA, Paris, France.
(λ x y . mail @ x y . nl) robbert krebbers