I am a post-doc, supervised by Lars Birkedal, in the Logic and Semantics group of Aarhus University. I am working on separation logic.

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.

This list contains some courses I have taught:

- Robbert Krebbers. The C standard formalized in Coq. Draft of PhD thesis.
- Robbert Krebbers. A Formal C Memory Model for Separation Logic. Accepted with revisions for JAR.
- Robbert Krebbers and Freek Wiedijk. A Typed C11 Semantics for Interactive Theorem Proving. In CPP, pages 15-27.

- Robbert Krebbers. Separation algebras for C verification in Coq. In VSTTE, volume 8471 of LNCS, pages 150-166.
- Robbert Krebbers, Xavier Leroy and Freek Wiedijk. Formal C semantics: CompCert and the C standard. In ITP, volume 8558 of LNCS, pages 543-548.
- Robbert Krebbers. An operational and axiomatic semantics for non-determinism and sequence points in C. In POPL, pages 101-112.

- 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. The λμT-calculus. 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.

- Robbert Krebbers. A call-by-value λ-calculus with lists and control. In CL&C, volume 97 of EPTCS, pages 19-33.

- Herman Geuvers and Robbert Krebbers. The correctness of Newman's typability algorithm and some of its extensions. In volume 412 of TCS, pages 3242-3261.
- Robbert Krebbers and Bas Spitters. Computer certified efficient exact reals in Coq. In CICM, volume 6824 of LNAI, pages 90-103.
- Robbert Krebbers and Freek Wiedijk. A Formalization of the C99 Standard in HOL, Isabelle and Coq. In CICM, volume 6824 of LNAI, pages 297-299.

- Robbert Krebbers. A formalization of Γ
_{∞}in Coq. Note. - Herman Geuvers, Robbert Krebbers, James McKinna and Freek Wiedijk. Pure Type Systems without Explicit Contexts. In LFMTP, volume 34 of EPTCS, pages 53-67.
- Robbert Krebbers. Classical logic, control calculi and data types. Master's thesis.

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.

- Formalizing C in Coq. At the Princeton PL reading group, Fri 24, 2014, Princeton University, Princeton, USA
- A Separation Logic for Non-determinism and Sequence Points in C Formalized in Coq. At TYPES, May 14, 2014, IHP, Paris, France
- 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.

- My GitHub repository
- CH
_{2}O: A formalization of the C11 standard in Coq - C-CORN: Coq Repository at Nijmegen
- Math classes

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