About

Robbert I am a (tenured) assistant professor at the department of software science at Radboud University Nijmegen. My research interests span many aspects of programming languages and 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 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.

I have received my PhD (cum laude) from Radboud University Nijmegen (2011-2015), have been a postdoc in the logic and semantics group at Aarhus University (2015-2016), and a (tenure-track) assistant professor in the programming languages group at Delft University of Technology (2016-2020).

News

I will move from TUDelft 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 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), Workshop "Static Analysis Meets Program Logics" (co-chair), CoqPL'19 (co-chair), POPL'19 (PC), PLNL'18 (co-chair), HOPE'17 (PC), POPL'17 (ERC + AEC), CPP'17 (PC), Coq Workshop'16 (PC).

Research group

Current PhD students:

Arjen Rouvoet: daily advisor/co-promotor (promotor: Eelco Visser)
Dan Frumin: daily advisor/first 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, 2019-2020, now formal methods engineer at BedRock systems)
Guillaume Ambal (intern, 2019, from ENS-Lyon)

Contact

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

Office: working from home due to covid

Send snail mail/packages to:

Dr. Robbert Krebbers
Department of Software Science
Institute for Computing and Information Sciences
Faculty of Science
Mailbox 47
PO Box 9010
6500 GL Nijmegen
The Netherlands