Robbert Krebbers

Registered user since Thu 16 Jun 2016

Name:Robbert Krebbers
Affiliation:Radboud University Nijmegen
Personal website:http://robbertkrebbers.nl
Research interests:Semantics, Separation logic, Theorem proving, Coq

Contributions

CPP 2022 Conference Chair in Organization Committee within the CPP 2022-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
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