Robbert Krebbers

75 papers A* 7A 3B 13C 1Journal 42Unranked 6
YearRankTypeTitle / Venue / Authors
2026 B conf
A Recipe for Modular Verification of Generic Tree Traversals.
CPP
Laila Elbeheiry, Michael Sammler, Robbert Krebbers, Derek Dreyer, Deepak Garg
2026 J jnl
A Relational Separation Logic for Effect Handlers.
Proc. ACM Program. Lang.
Paulo Emílio de Vilhena, Simcha van Collem, Ines Wright, Robbert Krebbers
2026 B conf
Building Blocks for Step-Indexed Program Logics.
CPP
Thomas Somers, Jonas Kastberg Hinrichsen, Lennard Gäher, Robbert Krebbers
2026 — ed.
Programming Languages and Systems - 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part I
ESOP (1)
Robbert Krebbers
2026 — ed.
Programming Languages and Systems - 35th European Symposium on Programming, ESOP 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II
ESOP (2)
Robbert Krebbers
2025 J jnl
Affect: An Affine Type and Effect System.
Proc. ACM Program. Lang.
Orpheas van Rooij, Robbert Krebbers
2025 B conf
Inductive Predicates via Least Fixpoints in Higher-Order Separation Logic.
ITP
Robbert Krebbers, Luko van der Maas, Enrico Tassi
2025 C conf
Mechanized Type Soundness for Substructural Types using Iris.
PPDP
Robbert Krebbers
2025 J jnl
Verified Interpreters for Dynamic Languages with Applications to the Nix Expression Language.
Proc. ACM Program. Lang.
Rutger Broekhoff, Robbert Krebbers
2024 J jnl
A Logical Approach to Type Soundness.
J. ACM
Amin Timany, Robbert Krebbers, Derek Dreyer, Lars Birkedal
2024 J jnl
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic.
Proc. ACM Program. Lang.
Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, Jeehoon Kang
2024 J jnl
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing.
Proc. ACM Program. Lang.
Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers
2024 — ed.
Logics and Type Systems in Theory and Practice - Essays Dedicated to Herman Geuvers on The Occasion of His 60th Birthday
Logics and Type Systems in Theory and Practice
Venanzio Capretta, Robbert Krebbers, Freek Wiedijk
2024 B conf
Modular Verification of Intrusive List and Tree Data Structures in Separation Logic.
ITP
Marc Hermes, Robbert Krebbers
2024 J jnl
Multris: Functional Verification of Multiparty Message Passing in Separation Logic.
Proc. ACM Program. Lang.
Jonas Kastberg Hinrichsen, Jules Jacobs, Robbert Krebbers
2024 J jnl
RefinedRust: A Type System for High-Assurance Verification of Rust Programs.
Proc. ACM Program. Lang.
Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer
2024 B conf
Unification for Subformula Linking under Quantifiers.
CPP
Ike Mulder, Robbert Krebbers
2024 J jnl
Verified Lock-Free Session Channels with Linking.
Proc. ACM Program. Lang.
Thomas Somers, Robbert Krebbers
2023 J jnl
Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic.
Proc. ACM Program. Lang.
Ike Mulder, Lukasz Czajka, Robbert Krebbers
2023 J jnl
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl).
Proc. ACM Program. Lang.
Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers
2023 J jnl
DimSum: A Decentralized Approach to Multi-language Semantics and Verification.
Proc. ACM Program. Lang.
Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer
2023 B conf
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk).
ITP
Robbert Krebbers
2023 B ed.
Proceedings of the 12th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2023, Boston, MA, USA, January 16-17, 2023
CPP
Robbert Krebbers, Dmitriy Traytel, Brigitte Pientka, Steve Zdancewic
2023 J jnl
Proof Automation for Linearizability in Separation Logic.
Proc. ACM Program. Lang.
Ike Mulder, Robbert Krebbers
2022 J jnl
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic.
Log. Methods Comput. Sci.
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
2022 J jnl
Connectivity graphs: a method for proving deadlock freedom based on separation logic.
Proc. ACM Program. Lang.
Jules Jacobs, Stephanie Balzer, Robbert Krebbers
2022 A* conf
Diaframe: automated verification of fine-grained concurrent programs in Iris.
PLDI
Ike Mulder, Robbert Krebbers, Herman Geuvers
2022 J jnl
Later credits: resourceful reasoning for the later modality.
Proc. ACM Program. Lang.
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
2022 J jnl
Multiparty GV: functional multiparty session types with certified deadlock freedom.
Proc. ACM Program. Lang.
Jules Jacobs, Stephanie Balzer, Robbert Krebbers
2022 J jnl
Simuliris: a separation logic framework for verifying concurrent program optimizations.
Proc. ACM Program. Lang.
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer
2022 J jnl
VIP: verifying real-world C idioms with integer-pointer casts.
Proc. ACM Program. Lang.
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell
2021 A* conf
Compositional Non-Interference for Fine-Grained Concurrent Programs.
SP
Dan Frumin, Robbert Krebbers, Lars Birkedal
2021 J jnl
Intrinsically typed compilation with nameless labels.
Proc. ACM Program. Lang.
Arjen Rouvoet, Robbert Krebbers, Eelco Visser
2021 B conf
Machine-checked semantic session typing.
CPP
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson
2021 J jnl
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity.
Log. Methods Comput. Sci.
Dan Frumin, Robbert Krebbers, Lars Birkedal
2021 A* conf
RefinedC: automating the foundational verification of C code with refined ownership types.
PLDI
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg
2021 J jnl
Safe systems programming in Rust.
Commun. ACM
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
2021 A* conf
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic.
PLDI
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
2020 J jnl
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic.
CoRR
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
2020 J jnl
Actris: session-type based reasoning in separation logic.
Proc. ACM Program. Lang.
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
2020 B conf
Intrinsically-typed definitional interpreters for linear, session-typed languages.
CPP
Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser
2020 J jnl
Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications.
Proc. ACM Program. Lang.
Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser
2020 J jnl
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity.
CoRR
Dan Frumin, Robbert Krebbers, Lars Birkedal
2020 J jnl
Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris.
Proc. ACM Program. Lang.
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers
2019 J jnl
A benchmark for C program verification.
CoRR
Marko C. J. D. van Eekelen, Daniil Frumin, Herman Geuvers, Léon Gondelman, Robbert Krebbers, Marc Schoolderman, Sjaak Smetsers, Freek Verbeek, Benoît Viguier, Freek Wiedijk
2019 J jnl
Compositional Non-Interference for Fine-Grained Concurrent Programs.
CoRR
Dan Frumin, Robbert Krebbers, Lars Birkedal
2019 J jnl
Iron: managing obligations in higher-order concurrent separation logic.
Proc. ACM Program. Lang.
Ales Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal
2019 A conf
Semi-automated Reasoning About Non-determinism in C Expressions.
ESOP
Dan Frumin, Léon Gondelman, Robbert Krebbers
2018 J jnl
Intrinsically-typed definitional interpreters for imperative languages.
Proc. ACM Program. Lang.
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, Eelco Visser
2018 J jnl
Iris from the ground up: A modular foundation for higher-order concurrent separation logic.
J. Funct. Program.
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer
2018 J jnl
MoSeL: a general, extensible modal framework for interactive proofs in separation logic.
Proc. ACM Program. Lang.
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
2018 J jnl
Mtac2: typed tactics for backward reasoning in Coq.
Proc. ACM Program. Lang.
Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer
2018 A* conf
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency.
LICS
Dan Frumin, Robbert Krebbers, Lars Birkedal
2018 J jnl
RustBelt: securing the foundations of the rust programming language.
Proc. ACM Program. Lang.
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
2017 A* conf
Interactive proofs in higher-order concurrent separation logic.
POPL
Robbert Krebbers, Amin Timany, Lars Birkedal
2017 A conf
The Essence of Higher-Order Concurrent Separation Logic.
ESOP
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
2016 J jnl
A Formal C Memory Model for Separation Logic.
J. Autom. Reason.
Robbert Krebbers
2016 A conf
Higher-order ghost state.
ICFP
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
2016 — conf
Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq.
Theory and Practice of Formal Methods
Robbert Krebbers, Louis Parlant, Alexandra Silva
2015 J jnl
A Formal C Memory Model for Separation Logic.
CoRR
Robbert Krebbers
2015 B conf
A Typed C11 Semantics for Interactive Theorem Proving.
CPP
Robbert Krebbers, Freek Wiedijk
2014 A* conf
An operational and axiomatic semantics for non-determinism and sequence points in C.
POPL
Robbert Krebbers
2014 B conf
Formal C Semantics: CompCert and the C Standard.
ITP
Robbert Krebbers, Xavier Leroy, Freek Wiedijk
2014 — conf
Separation Algebras for C Verification in Coq.
VSTTE
Robbert Krebbers
2013 B conf
Aliasing Restrictions of C11 Formalized in Coq.
CPP
Robbert Krebbers
2013 B conf
Separation Logic for Non-local Control Flow and Block Scope Variables.
FoSSaCS
Robbert Krebbers, Freek Wiedijk
2013 J jnl
The
Ann. Pure Appl. Log.
Herman Geuvers, Robbert Krebbers, James McKinna
2012 — conf
A call-by-value lambda-calculus with lists and control
CL&C
Robbert Krebbers
2012 J jnl
The lambda-mu-T-calculus
CoRR
Herman Geuvers, Robbert Krebbers, James McKinna
2011 — conf
A Formalization of the C99 Standard in HOL, Isabelle and Coq.
Calculemus/MKM
Robbert Krebbers, Freek Wiedijk
2011 — conf
Computer Certified Efficient Exact Reals in Coq.
Calculemus/MKM
Robbert Krebbers, Bas Spitters
2011 J jnl
Computer certified efficient exact reals in Coq
CoRR
Robbert Krebbers, Bas Spitters
2011 J jnl
The correctness of Newman's typability algorithm and some of its extensions.
Theor. Comput. Sci.
Herman Geuvers, Robbert Krebbers
2011 J jnl
Type classes for efficient exact real arithmetic in Coq
Log. Methods Comput. Sci.
Robbert Krebbers, Bas Spitters
2010 — conf
Pure Type Systems without Explicit Contexts
LFMTP
Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk