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