Robbert Krebbers

Publication Activity (10 Years)

Years Active: 2010-2024
Publications (10 Years): 44

Top Topics

Concurrent Programs

Automated Reasoning

Lambda Calculus

Top Venues

Proc. ACM Program. Lang.

Publications

Ike Mulder, Robbert Krebbers
Unification for Subformula Linking under Quantifiers. CPP (2024)
Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer
RefinedRust: A Type System for High-Assurance Verification of Rust Programs. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, Jeehoon Kang
A Proof Recipe for Linearizability in Relaxed Memory Separation Logic. Proc. ACM Program. Lang. 8 (PLDI) (2024)
Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing. Proc. ACM Program. Lang. 8 (POPL) (2024)
Ike Mulder, Robbert Krebbers
Proof Automation for Linearizability in Separation Logic. Proc. ACM Program. Lang. 7 (OOPSLA1) (2023)
Ike Mulder, Lukasz Czajka, Robbert Krebbers
Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic. Proc. ACM Program. Lang. 7 (PLDI) (2023)
Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers
Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl). Proc. ACM Program. Lang. 7 (ICFP) (2023)
Robbert Krebbers
Interactive and Automated Proofs in Modal Separation Logic (Invited Talk). ITP (2023)
Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer
DimSum: A Decentralized Approach to Multi-language Semantics and Verification. Proc. ACM Program. Lang. 7 (POPL) (2023)
Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
Later credits: resourceful reasoning for the later modality. Proc. ACM Program. Lang. 6 (ICFP) (2022)
Jules Jacobs, Stephanie Balzer, Robbert Krebbers
Multiparty GV: functional multiparty session types with certified deadlock freedom. Proc. ACM Program. Lang. 6 (ICFP) (2022)
Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell
VIP: verifying real-world C idioms with integer-pointer casts. Proc. ACM Program. Lang. 6 (POPL) (2022)
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. Log. Methods Comput. Sci. 18 (2) (2022)
Ike Mulder, Robbert Krebbers, Herman Geuvers
Diaframe: automated verification of fine-grained concurrent programs in Iris. PLDI (2022)
Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer
Simuliris: a separation logic framework for verifying concurrent program optimizations. Proc. ACM Program. Lang. 6 (POPL) (2022)
Jules Jacobs, Stephanie Balzer, Robbert Krebbers
Connectivity graphs: a method for proving deadlock freedom based on separation logic. Proc. ACM Program. Lang. 6 (POPL) (2022)
Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal
Transfinite Iris: resolving an existential dilemma of step-indexed separation logic. PLDI (2021)
Arjen Rouvoet, Robbert Krebbers, Eelco Visser
Intrinsically typed compilation with nameless labels. Proc. ACM Program. Lang. 5 (POPL) (2021)
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
Safe systems programming in Rust. Commun. ACM 64 (4) (2021)
Dan Frumin, Robbert Krebbers, Lars Birkedal
Compositional Non-Interference for Fine-Grained Concurrent Programs. IEEE Symposium on Security and Privacy (2021)
Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg
RefinedC: automating the foundational verification of C code with refined ownership types. PLDI (2021)
Dan Frumin, Robbert Krebbers, Lars Birkedal
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. Log. Methods Comput. Sci. 17 (3) (2021)
Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson
Machine-checked semantic session typing. CPP (2021)
Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser
Intrinsically-typed definitional interpreters for linear, session-typed languages. CPP (2020)
Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser
Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications. Proc. ACM Program. Lang. 4 (OOPSLA) (2020)
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
Actris: session-type based reasoning in separation logic. Proc. ACM Program. Lang. 4 (POPL) (2020)
Dan Frumin, Robbert Krebbers, Lars Birkedal
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity. CoRR (2020)
Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers
Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris. Proc. ACM Program. Lang. 4 (ICFP) (2020)
Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic. CoRR (2020)
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
A benchmark for C program verification. CoRR (2019)
Dan Frumin, Léon Gondelman, Robbert Krebbers
Semi-automated Reasoning About Non-determinism in C Expressions. ESOP (2019)
Dan Frumin, Robbert Krebbers, Lars Birkedal
Compositional Non-Interference for Fine-Grained Concurrent Programs. CoRR (2019)
Ales Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal
Iron: managing obligations in higher-order concurrent separation logic. Proc. ACM Program. Lang. 3 (POPL) (2019)
Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer
Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 (2018)
Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer
RustBelt: securing the foundations of the rust programming language. Proc. ACM Program. Lang. 2 (POPL) (2018)
Dan Frumin, Robbert Krebbers, Lars Birkedal
ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency. LICS (2018)
Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, Eelco Visser
Intrinsically-typed definitional interpreters for imperative languages. Proc. ACM Program. Lang. 2 (POPL) (2018)
Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer
MoSeL: a general, extensible modal framework for interactive proofs in separation logic. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer
Mtac2: typed tactics for backward reasoning in Coq. Proc. ACM Program. Lang. 2 (ICFP) (2018)
Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal
The Essence of Higher-Order Concurrent Separation Logic. ESOP (2017)
Robbert Krebbers, Amin Timany, Lars Birkedal
Interactive proofs in higher-order concurrent separation logic. POPL (2017)
Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer
Higher-order ghost state. ICFP (2016)
Robbert Krebbers
A Formal C Memory Model for Separation Logic. J. Autom. Reason. 57 (4) (2016)
Robbert Krebbers, Louis Parlant, Alexandra Silva
Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq. Theory and Practice of Formal Methods (2016)
Robbert Krebbers
A Formal C Memory Model for Separation Logic. CoRR (2015)
Robbert Krebbers, Freek Wiedijk
A Typed C11 Semantics for Interactive Theorem Proving. CPP (2015)
Robbert Krebbers, Xavier Leroy, Freek Wiedijk
Formal C Semantics: CompCert and the C Standard. ITP (2014)
Robbert Krebbers
Separation Algebras for C Verification in Coq. VSTTE (2014)
Robbert Krebbers
An operational and axiomatic semantics for non-determinism and sequence points in C. POPL (2014)
Robbert Krebbers
Aliasing Restrictions of C11 Formalized in Coq. CPP (2013)
Robbert Krebbers, Freek Wiedijk
Separation Logic for Non-local Control Flow and Block Scope Variables. FoSSaCS (2013)
Herman Geuvers, Robbert Krebbers, James McKinna
-calculus. Ann. Pure Appl. Log. 164 (6) (2013)
Robbert Krebbers
A call-by-value lambda-calculus with lists and control CL&C (2012)
Herman Geuvers, Robbert Krebbers, James McKinna
The lambda-mu-T-calculus CoRR (2012)
Robbert Krebbers, Bas Spitters
Computer certified efficient exact reals in Coq CoRR (2011)
Robbert Krebbers, Bas Spitters
Type classes for efficient exact real arithmetic in Coq Log. Methods Comput. Sci. 9 (1) (2011)
Robbert Krebbers, Bas Spitters
Computer Certified Efficient Exact Reals in Coq. Calculemus/MKM (2011)
Robbert Krebbers, Freek Wiedijk
A Formalization of the C99 Standard in HOL, Isabelle and Coq. Calculemus/MKM (2011)
Herman Geuvers, Robbert Krebbers
The correctness of Newman's typability algorithm and some of its extensions. Theor. Comput. Sci. 412 (28) (2011)
Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk
Pure Type Systems without Explicit Contexts LFMTP (2010)