Publications

2024

• Jules Jacobs, Jonas Kastberg Hinrichsen and Robbert Krebbers. Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).
  [pdf] [coq sources]
• Ike Mulder and Robbert Krebbers. Unification for Subformula Linking under Quantifiers. In ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP).
  [pdf] [coq sources]
• Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers and Jeehong Kang. A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. In ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI).
  [pdf] [coq sources]
• Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers and Derek Dreyer. RefinedRust: A Type System for High-Assurance Verification of Rust Programs. In ACM SIGPLAN International Conference on Programming Language Design and Implementation (PLDI).
  [pdf] [coq sources]
• Amin Timany, Robbert Krebbers, Derek Dreyer and Lars Birkedal. A Logical Approach to Type Soundness. In Journal of the ACM (JACM).
  [pdf]
• Marc Hermes and Robbert Krebbers. Modular Verification of Intrusive List and Tree Data Structures in Separation Logic. In International Conference on Interactive Theorem Proving (ITP).
  [pdf]
• Jonas Kastberg Hinrichsen, Jules Jacobs and Robbert Krebbers. Multris: Functional Verification of Multiparty Message Passing in Separation Logic. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA).
  [pdf]
• Thomas Somers and Robbert Krebbers. Verified Lock-Free Session Channels with Linking. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA).
  [pdf]

2023

• Ike Mulder and Robbert Krebbers. Proof Automation for Linearizability in Separation Logic. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA). Recipient of the OOPSLA 2023 Distinguished Artifact Award.
  [pdf] [coq sources]
• Jules Jacobs, Jonas Kastberg Hinrichsen and Robbert Krebbers. Dependent Session Protocols in Separation Logic from First Principles. In ACM SIGPLAN International Conference on Functional Programming (ICFP).
  [pdf] [coq sources]
• Ike Mulder, Łukasz Czajka and Robbert Krebbers. Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).
  [pdf] [coq sources]
• Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg and Derek Dreyer. DimSum: A Decentralized Approach to Multi-language Semantics and Verification. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). Recipient of the POPL 2023 Distinguished Paper Award.
  [pdf] [coq sources]

2022

• Jules Jacobs, Stephanie Balzer and Robbert Krebbers. Multiparty GV: Functional Multiparty Session Types with Certified Deadlock Freedom. In ACM SIGPLAN International Conference on Functional Programming (ICFP).
  [pdf] [coq sources]
• Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal and Derek Dreyer. Later Credits: Resourceful Reasoning for the Later Modality. In ACM SIGPLAN International Conference on Functional Programming (ICFP).
  [pdf] [coq sources]
• Ike Mulder, Robbert Krebbers and Herman Geuvers. Diaframe: Automated Verification of Fine-Grained Concurrent Programs in Iris. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).
  [pdf] [coq sources]
• Jules Jacobs, Stephanie Balzer and Robbert Krebbers. Connectivity Graphs: A Method for Proving Deadlock Freedom Based on Separation Logic. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).
  [pdf] [coq sources]
• Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer and Peter Sewell. VIP: Verifying Real-World C Idioms with Integer-Pointer Casts. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).
  [pdf] [coq sources]
• Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hai Dang, Robbert Krebbers, Jeehong Kang and Derek Dreyer. Simuliris: A Separation Logic Framework for Verifying Concurrent Program Optimizations. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL). Recipient of the POPL 2022 Distinguished Paper Award.
  [pdf] [coq sources]
• Jonas Kastberg Hinrichsen, Jesper Bengtson and Robbert Krebbers. Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. In Logical Methods in Computer Science (LMCS).
  [pdf] [coq sources]

2021

• Arjen Rouvoet, Robbert Krebbers and Eelco Visser. Intrinsically Typed Compilation with Nameless Labels. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).
  [pdf] [agda sources] [website]
• Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers and Jesper Bengtson. Machine-Checked Semantic Session Typing. In ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP).
  Recipient of CPP 2021 Distinguished Paper Award.
  [pdf] [coq sources]
• Dan Frumin, Robbert Krebbers and Lars Birkedal. Compositional Non-Interference for Fine-Grained Concurrent Programs. In IEEE Symposium on Security and Privacy (SP).
  [pdf] [coq sources]
• Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers and Derek Dreyer. Safe Systems Programming in Rust: The Promise and the Challenge. In Communications of the ACM (CACM).
  [pdf] [html + video]
• Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer and Lars Birkedal. Transfinite Iris: Resolving an Existential Dilemma of Step-Indexed Separation Logic. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI).
  
  [pdf] [website] [coq sources]
• Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer and Deepak Garg. RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types. In ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). Recipient of the PLDI 2021 Distinguished Paper Award and the PLDI 2021 Distinguished Artifact Award.
  [pdf] [website] [coq sources]
• Dan Frumin, Robbert Krebbers and Lars Birkedal. ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. In Logical Methods in Computer Science (LMCS).
  [pdf] [website] [coq sources]

2020

• Jonas Kastberg Hinrichsen, Jesper Bengtson and Robbert Krebbers. Actris: Session-Type Based Reasoning in Separation Logic. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).
  [pdf] [coq sources]
• Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers and Eelco Visser. Intrinsically-Typed Definitional Interpreters for Linear, Session-Typed Languages. In ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP).
  [pdf] [agda sources]
• Paolo Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal and Robbert Krebbers. Scala Step-by-Step: Soundness for DOT with Step-Indexed Logical Relations in Iris. In ACM SIGPLAN International Conference on Functional Programming (ICFP).
  [pdf] [coq sources]
• Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers and Eelco Visser. Knowing When to Ask: Sound Scheduling Name Resolution Queries in Type Checkers Derived From Declarative Specifications. In ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications (OOPSLA).
  [pdf] [website]

2019

• Dan Frumin, Léon Gondelman and Robbert Krebbers. Semi-Automated Reasoning About Non-Determinism in C Expressions. In European Symposium on Programming (ESOP).
  [pdf] [coq sources]
• Aleš Bizjak, Daniel Gratzer, Robbert Krebbers and Lars Birkedal. Iron: Managing Obligations in Higher-Order Concurrent Separation Logic. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).
  [pdf] [website] [coq sources]

2018

• Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud and Derek Dreyer. MoSeL: A General, Extensible Modal Framework for Interactive Proofs in Separation Logic. In ACM SIGPLAN International Conference on Functional Programming (ICFP).
  [pdf] [slides] [website] [coq sources]
• Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas and Derek Dreyer. Mtac2: Typed Tactics for Backward Reasoning in Coq. In ACM SIGPLAN International Conference on Functional Programming (ICFP).
  [pdf] [coq sources]
• Dan Frumin, Robbert Krebbers and Lars Birkedal. ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. In ACM/IEEE Symposium on Logic in Computer Science (LICS).
  [pdf] [website] [coq sources]
• Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers and Derek Dreyer. RustBelt: Securing the Foundations of the Rust Programming Language. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).
  [pdf] [website] [coq sources]
• Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers and Eelco Visser. Intrinsically-Typed Definitional Interpreters for Imperative Languages. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).
  [pdf] [agda sources]
• Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Aleš Bizjak, Lars Birkedal and Derek Dreyer. Iris From The Ground Up: A Modular Foundation for Higher-Order Concurrent Separation Logic. In Journal of Functional Programming (JFP).
  [pdf] [coq sources]

2017

• Robbert Krebbers, Ralf Jung, Aleš Bizjak, Jacques-Henri Jourdan, Derek Dreyer and Lars Birkedal. The Essence of Higher-Order Concurrent Separation Logic. In European Symposium on Programming (ESOP).
  [pdf] [slides] [coq sources]
• Robbert Krebbers, Amin Timany and Lars Birkedal. Interactive Proofs in Higher-Order Concurrent Separation Logic. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).
  [pdf] [at publisher] [slides] [coq sources] [coq sources logical relations]

2016

• Ralf Jung, Robbert Krebbers, Lars Birkedal and Derek Dreyer. Higher-Order Ghost State. In ACM SIGPLAN International Conference on Functional Programming (ICFP).
  [pdf] [at publisher] [coq sources]
• Robbert Krebbers. A Formal C Memory Model for Separation Logic. In Journal of Automated Reasoning (JAR).
  [pdf] [at publisher] [coq sources]
• Robbert Krebbers, Louis Parlant and Alexandra Silva. Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq. In Theory and Practice of Formal Methods Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday.
  [pdf] [at publisher] [coq sources]

2015

• Robbert Krebbers. The C Standard Formalized in Coq. PhD thesis. Radboud University Nijmegen. Defended with cum laude distinction.
  [pdf] [coq sources]
• Robbert Krebbers. The Hypergame Paradox in Coq. Liber Amicorum for Henk Barendregt.
  [pdf] [coq sources]
• Robbert Krebbers and Freek Wiedijk. A Typed C11 Semantics for Interactive Theorem Proving. In ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP).
  [pdf] [at publisher] [slides] [coq sources]

2014

• Robbert Krebbers. Separation Algebras for C Verification in Coq. In Verified Software: Theories, Tools and Experiments (VSTTE).
  [pdf] [at publisher] [slides] [coq sources]
• Robbert Krebbers, Xavier Leroy and Freek Wiedijk. Formal C Semantics: CompCert and the C Standard. In International Conference on Interactive Theorem Proving (ITP).
  [pdf] [at publisher] [slides] [coq sources]
• Robbert Krebbers. An Operational and Axiomatic Semantics for Non-Determinism and Sequence Points in C. In ACM SIGPLAN Symposium on Principles of Programming Languages (POPL).
  [pdf] [at publisher] [slides] [coq sources]

2013

• Robbert Krebbers. Aliasing Restrictions of C11 Formalized in Coq. In ACM SIGPLAN International Conference on Certified Programs and Proofs (CPP).
  [pdf] [at publisher] [slides] [coq sources]
• Robbert Krebbers and Freek Wiedijk. Separation Logic for Non-local Control Flow and Block Scope Variables. In International Conference on Foundations of Software Science and Computation Structures (FoSSaCS).
  Recipient of best student contribution.
  [pdf] [at publisher] [slides] [coq sources] [documentation]
• Herman Geuvers, Robbert Krebbers and James McKinna. The λμT-calculus. In Annals of Pure and Applied Logic (APAL).
  [pdf] [at publisher]
• Robbert Krebbers and Bas Spitters. Type Classes for Efficient Exact Real Arithmetic in Coq. In Logical Methods in Computer Science (LMCS).
  [pdf] [at publisher] [coq sources]

2012

• Robbert Krebbers. A Call-by-value λ-calculus with Lists and Control. In Workshop on Classical Logic and Computation (CL&C).
  [pdf] [at publisher] [slides]

2011

• Herman Geuvers and Robbert Krebbers. The Correctness of Newman's Typability Algorithm and Some of Its Extensions. In Theoretical Computer Science (TCS).
  [pdf] [at publisher]
• Robbert Krebbers and Bas Spitters. Computer Certified Efficient Exact Reals in Coq. In International Conference on Intelligent Computer Mathematics (CICM).
  [pdf] [at publisher] [slides] [coq sources]
• Robbert Krebbers and Freek Wiedijk. A Formalization of the C99 Standard in HOL, Isabelle and Coq. In International Conference on Intelligent Computer Mathematics (CICM).
  [pdf] [at publisher] [poster] [slides]

2010

• Robbert Krebbers. A formalization of Γ_∞ in Coq. Note.
  [pdf] [coq formalization]
• Herman Geuvers, Robbert Krebbers, James McKinna and Freek Wiedijk. Pure Type Systems without Explicit Contexts. In Logical Frameworks and Meta-languages: Theory and Practice (LFMTP).
  [pdf] [at publisher] [slides]
• Robbert Krebbers. Classical Logic, Control Calculi and Data Types. Master's thesis.
  [pdf] [slides]