About

Robbert I am an assistant professor in the programming languages group at the department of software technology at Delft University of Technology. My research interests span many aspects of program verification, for example:

Semantics of real programming languages: In my PhD thesis, I have developed a semantics and separation logic for a large fragment of the C programming language. More recently, I have contributed to Rustbelt: the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust.
Multilingual software: I have recently been awarded a prestigious Dutch NWO Veni grant (250.000 EUR) to work on the semantics and reasoning principles for interaction between different programming languages via shared-memory and asynchronous message passing.
Concurrent separation logic: I am one of the main developers of the Iris framework for concurrent separation logic in Coq, which has been deployed very effectively in a wide variety of verification projects. These projects include but are not limited to: verification of fine-grained concurrent data structures, logical-relations for relational reasoning, program logics for relaxed memory models, program logics for object capabilities, and a safety proof for a realistic subset of the Rust programming language. Take a look at the Iris website for the many exciting applications of Iris.
Proof assistants: I am an active user of the Coq proof assistant; nearly all of my research has a corresponding mechanization in Coq. Moreover, I am the main developer of coq-std++: an extended standard library for Coq.
Tactic languages: In order to carry out proofs at the right level of abstraction, I have worked on the development of various tactics languages for the Coq proof assistant. Notably, I am the designer of the MoSeL (formerly Iris Proof Mode) tactic language for separation logic proofs in Coq, and have contributed to Mtac2, a next-generation tactic language with support for strongly typed tactic programming.

Before becoming an assistant professor at TUDelft, I have received my PhD (cum laude) from Radboud University Nijmegen under the supervision of Freek Wiedijk and Herman Geuvers, and have been a postdoc in Lars Birkedal's group at Aarhus University.

News

I will move to Radboud University Nijmegen (1 September 2020).
Ike Mulder has joined my team as a PhD student (1 May 2020).
I will be on the program committee of ESOP'21 and FSCD'21.
I have been invited to give a keynote at ADSL'20 (collocated with POPL'20 in New Orleans).
Together with Lars Birkedal, I am organizing the first edition of the Iris workshop 28 Oct-1 Nov in Aarhus.
I will be on the program committee of ICFP'20.
Jules Jacobs has joined my team as a PhD student (1 September 2019).
I am (co-)organizing CoqPL'20 and PLMW'20 (both collocated with POPL'20 in New Orleans).
I have organized the workshop Effective Verification: Static Analysis Meets Program Logics at the Lorentz Center.
Paolo Giarrusso has joined my team as a post-doc (1 April 2019).
I am (co-)organizing CoqPL'19 (collocated with POPL'19 in Lisbon). Please attend!
I have been awarded a prestigious Dutch NWO Veni grant (250.000 EUR).

Professional service

ESOP'21 (PC), FSCD'21 (PC), ICFP'20 (PC), PLMW'20 (co-chair), CoqPL'20 (co-chair), PLNL'19 (PC), Iris Workshop'19 (co-chair), CoqPL'19 (co-chair), PLNL'18 (co-chair), POPL'19 (PC), HOPE'17 (PC), POPL'17 (ERC + AEC), CPP'17 (PC), Coq Workshop'16 (PC).

Research group

PhD students:

Arjen Rouvoet (daily advisor/co-promotor, promotor: Eelco Visser)
Dan Frumin (daily advisor/co-promotor, second co-promotor: Freek Wiedijk, promotor: Herman Geuvers)
Jules Jacobs (daily advisor/co-promotor, promotor: Herman Geuvers)
Ike Mulder (daily advisor/co-promotor, promotor: Herman Geuvers)
Jonas Kastberg Hinrichsen (external advisor, daily advisor at ITU: Jesper Bengtson)

Alumni:

Paolo Giarrusso (postdoc, now formal methods engineer at BedRock systems)
Guillaume Ambal (intern from ENS-Lyon)

Contact

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

Office: room E04.400, Building 28, Van Mourik Broekmanweg 6, Delft

Send mail/packages to:

Dr. Robbert Krebbers
EEMCS, Software Technology
P.O. Box 5031, 2600 GA Delft
The Netherlands