Robbert Krebbers

Registered user since Thu 16 Jun 2016

Name:Robbert Krebbers
Bio:

I am an associate professor at the department of software science at Radboud University Nijmegen, The Netherlands.

My research is centered around scaling up program verification techniques to challenging programming paradigms like concurrency, higher-order functions and modules, and applying these techniques to programming languages like C, Rust, and Scala. I like to build solid mathematical foundations and usable tools, preferably using the Coq proof assistant.

The main research project I am the co-designer and co-leader of is Iris: a framework for concurrent separation logic in Coq. Iris has been deployed in a wide variety of verification projects, for many different programming languages, at many different institutes world-wide. Check out the Iris website for more information!

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 an assistant professor in the programming languages group at Delft University of Technology (2016-2020).

Country:Netherlands
Affiliation:Radboud University Nijmegen
Research interests:Semantics, Separation logic, Theorem proving, Coq

Contributions

POPL 2023 Committee Member in Program Committee within the POPL-track
PLDI 2022 Author of (PLDI 2021) RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types within the SIGPLAN Track-track
Author of (PLDI 2021) Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic within the SIGPLAN Track-track
Author of Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris within the PLDI-track
PLMW 2022 Committee Member in Organizing Committee within the PLMW 2022-track
Session Chair of Morning 1 (part of PLMW 2022)
CPP 2022 Conference Chair in Organization Committee within the CPP 2022-track
Session Chair of Chairs' Report and Business Meeting (part of CPP 2022)
Session Chair of Welcome from the chairs (part of CPP 2022)
POPL 2022 Author of Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic within the POPL-track
Author of VIP: Verifying Real-World C Idioms with Integer-Pointer Casts within the POPL-track
Author of Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations within the POPL-track
PLDI 2021 Author of RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types within the PLDI-track
Author of Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic within the PLDI-track
CPP 2021 Author of Machine-Checked Semantic Session Typing within the CPP 2021-track
POPL 2021 Author of Intrinsically Typed Compilation with Nameless Labels within the POPL-track
SPLASH 2022 Committee Member in Review Committee within the OOPSLA-track
PLNL 2019 Committee Member in Program Committee within the PLNL-track
SPLASH 2020 Author of Knowing When to Ask: Artifact within the OOPSLA Artifacts-track
Author of Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative Specifications within the OOPSLA-track
Author of Knowing When to Ask: Sound Scheduling of Name Resolution in Type Checkers Derived from Declarative Specifications within the Posters-track
CoqPL 2020 Co-chair in Organizing Committee within the CoqPL-track
Session Chair of Contributed Talks & Coq Developers (part of CoqPL)
Session Chair of Invited Talk (part of CoqPL)
PLMW 2020 Organizer in Organizing Committee within the PLMW 2020-track
Session Chair of Morning 2 (part of PLMW 2020)
ADSL 2020 Author of Relational reasoning using concurrent separation logic within the ADSL 2020-track
ICFP 2020 Committee Member in Program Committee within the ICFP Program-track
Author of Scala Step-by-Step — Soundness for DOT with Step-Indexed Logical Relations in Iris within the ICFP Program-track
CPP 2020 Author of Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages within the CPP 2020-track
POPL 2020 Committee Member in Organizing Committee within the Mentoring Breakfasts-track
Author of [T4] Proving Semantic Type Soundness in Iris within the TutorialFest-track
Author of Actris: Session-Type Based Reasoning in Separation Logic within the Research Papers-track
PLNL 2018 Organizer in Organizing Committee within the PLNL-track
Session Chair of 3 (part of PLNL)
CoqPL 2019 Co-chair in Organizing Committee within the CoqPL-track
Session Chair of Contributed Talks 4 (part of CoqPL)
ESOP 2019 Author of Semi-Automated Reasoning About Non-Determinism in C Expressions within the ESOP 2019-track
POPL 2019 Session Chair of Synthesis (part of Research Papers)
Committee Member in Program Committee within the Research Papers-track
Author of Iron: Managing Obligations in Higher-Order Concurrent Separation Logic within the Research Papers-track
CoqPL 2018 Author of A calculus for logical refinements in separation logic within the -track
ICFP 2018 Author of Mtac2: Typed Tactics for Backward Reasoning in Coq within the Research Papers-track
Author of MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic within the Research Papers-track
HOPE 2017 Committee Member in Program Committee within the HOPE 2017-track
Author of RustBelt: Securing the Foundations of the Rust Programming Language within the HOPE 2017-track
POPL 2018 Author of Intrinsically-Typed Definitional Interpreters within the Artifact Evaluation-track
Author of Iris - A Modular Foundation for Higher-Order Concurrent Separation Logic. within the TutorialFest-track
Author of Intrinsically-Typed Definitional Interpreters for Imperative Languages within the Research Papers-track
Author of RustBelt: Securing the Foundations of the Rust Programming Language within the Artifact Evaluation-track
Author of RustBelt: Securing the Foundations of the Rust Programming Language within the Research Papers-track
CPP 2017 Committee Member in Program Committee within the CPP-track
TTT 2017 Invited Speaker of Invited Talk -- Iris: a framework for higher-order concurrent separation logic in Coq within the TTT-track
CoqPL 2017 Author of Logical Relations in Iris within the CoqPL 2017-track
Invited Speaker of Invited Talk -- Demonstration of the Iris separation logic in Coq within the CoqPL 2017-track
POPL 2017 Committee Member in Artifact Evaluation Committee within the Artifact Evaluation-track
Author of Interactive Proofs in Higher-Order Concurrent Separation Logic within the POPL-track
ERC member in External Review Committee within the POPL-track
ICFP 2016 Author of Higher-Order Ghost State within the Research Papers-track