Robbert Krebbers

According to our database, Robbert Krebbers authored at least 59 papers between 2010 and 2024.

Collaborative distances:

• Dijkstra number of four.
• Erdős number of four.

2024

A Logical Approach to Type Soundness.

Amin Timany, Robbert Krebbers, Derek Dreyer, Lars Birkedal

J. ACM, December, 2024

Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing.

Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers

Proc. ACM Program. Lang., January, 2024

Verified Lock-Free Session Channels with Linking.

Thomas Somers, Robbert Krebbers

Proc. ACM Program. Lang., 2024

A Proof Recipe for Linearizability in Relaxed Memory Separation Logic.

Sunho Park, Jaewoo Kim, Ike Mulder, Jaehwang Jung, Janggun Lee, Robbert Krebbers, Jeehoon Kang

Proc. ACM Program. Lang., 2024

Multris: Functional Verification of Multiparty Message Passing in Separation Logic.

Jonas Kastberg Hinrichsen, Jules Jacobs, Robbert Krebbers

Proc. ACM Program. Lang., 2024

RefinedRust: A Type System for High-Assurance Verification of Rust Programs.

Lennard Gäher, Michael Sammler, Ralf Jung, Robbert Krebbers, Derek Dreyer

Proc. ACM Program. Lang., 2024

Modular Verification of Intrusive List and Tree Data Structures in Separation Logic.

Marc Hermes, Robbert Krebbers

Proceedings of the 15th International Conference on Interactive Theorem Proving, 2024

Unification for Subformula Linking under Quantifiers.

Ike Mulder, Robbert Krebbers

Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2024

2023

Dependent Session Protocols in Separation Logic from First Principles (Functional Pearl).

Jules Jacobs, Jonas Kastberg Hinrichsen, Robbert Krebbers

Proc. ACM Program. Lang., August, 2023

Proof Automation for Linearizability in Separation Logic.

Ike Mulder, Robbert Krebbers

Proc. ACM Program. Lang., April, 2023

DimSum: A Decentralized Approach to Multi-language Semantics and Verification.

Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers, Deepak Garg, Derek Dreyer

Proc. ACM Program. Lang., January, 2023

Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic.

Ike Mulder, Lukasz Czajka, Robbert Krebbers

Proc. ACM Program. Lang., 2023

Interactive and Automated Proofs in Modal Separation Logic (Invited Talk).

Robbert Krebbers

Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2022

Later credits: resourceful reasoning for the later modality.

Simon Spies, Lennard Gäher, Joseph Tassarotti, Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer

Proc. ACM Program. Lang., 2022

VIP: verifying real-world C idioms with integer-pointer casts.

Rodolphe Lepigre, Michael Sammler, Kayvan Memarian, Robbert Krebbers, Derek Dreyer, Peter Sewell

Proc. ACM Program. Lang., 2022

Multiparty GV: functional multiparty session types with certified deadlock freedom.

Jules Jacobs, Stephanie Balzer, Robbert Krebbers

Proc. ACM Program. Lang., 2022

Connectivity graphs: a method for proving deadlock freedom based on separation logic.

Jules Jacobs, Stephanie Balzer, Robbert Krebbers

Proc. ACM Program. Lang., 2022

Simuliris: a separation logic framework for verifying concurrent program optimizations.

Lennard Gäher, Michael Sammler, Simon Spies, Ralf Jung, Hoang-Hai Dang, Robbert Krebbers, Jeehoon Kang, Derek Dreyer

Proc. ACM Program. Lang., 2022

Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic.

Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers

Log. Methods Comput. Sci., 2022

Diaframe: automated verification of fine-grained concurrent programs in Iris.

Ike Mulder, Robbert Krebbers, Herman Geuvers

Proceedings of the PLDI '22: 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation, San Diego, CA, USA, June 13, 2022

2021

Intrinsically typed compilation with nameless labels.

Arjen Rouvoet, Robbert Krebbers, Eelco Visser

Proc. ACM Program. Lang., 2021

ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity.

Dan Frumin, Robbert Krebbers, Lars Birkedal

Log. Methods Comput. Sci., 2021

Safe systems programming in Rust.

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer

Commun. ACM, 2021

Compositional Non-Interference for Fine-Grained Concurrent Programs.

Dan Frumin, Robbert Krebbers, Lars Birkedal

Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic.

Simon Spies, Lennard Gäher, Daniel Gratzer, Joseph Tassarotti, Robbert Krebbers, Derek Dreyer, Lars Birkedal

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

RefinedC: automating the foundational verification of C code with refined ownership types.

Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian, Derek Dreyer, Deepak Garg

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Machine-checked semantic session typing.

Jonas Kastberg Hinrichsen, Daniël Louwrink, Robbert Krebbers, Jesper Bengtson

Proceedings of the CPP '21: 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2021

2020

Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications.

Arjen Rouvoet, Hendrik van Antwerpen, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser

Proc. ACM Program. Lang., 2020

Actris: session-type based reasoning in separation logic.

Jonas Kastberg Hinrichsen, Jesper Bengtson, Robbert Krebbers

Proc. ACM Program. Lang., 2020

Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris.

Paolo G. Giarrusso, Léo Stefanesco, Amin Timany, Lars Birkedal, Robbert Krebbers

Proc. ACM Program. Lang., 2020

Intrinsically-typed definitional interpreters for linear, session-typed languages.

Arjen Rouvoet, Casper Bach Poulsen, Robbert Krebbers, Eelco Visser

Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019

Iron: managing obligations in higher-order concurrent separation logic.

Ales Bizjak, Daniel Gratzer, Robbert Krebbers, Lars Birkedal

Proc. ACM Program. Lang., 2019

A benchmark for C program verification.

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

CoRR, 2019

Semi-automated Reasoning About Non-determinism in C Expressions.

Dan Frumin, Léon Gondelman, Robbert Krebbers

Proceedings of the Programming Languages and Systems, 2019

2018

Intrinsically-typed definitional interpreters for imperative languages.

Casper Bach Poulsen, Arjen Rouvoet, Andrew Tolmach, Robbert Krebbers, Eelco Visser

Proc. ACM Program. Lang., 2018

MoSeL: a general, extensible modal framework for interactive proofs in separation logic.

Robbert Krebbers, Jacques-Henri Jourdan, Ralf Jung, Joseph Tassarotti, Jan-Oliver Kaiser, Amin Timany, Arthur Charguéraud, Derek Dreyer

Proc. ACM Program. Lang., 2018

Mtac2: typed tactics for backward reasoning in Coq.

Jan-Oliver Kaiser, Beta Ziliani, Robbert Krebbers, Yann Régis-Gianas, Derek Dreyer

Proc. ACM Program. Lang., 2018

RustBelt: securing the foundations of the rust programming language.

Ralf Jung, Jacques-Henri Jourdan, Robbert Krebbers, Derek Dreyer

Proc. ACM Program. Lang., 2018

Iris from the ground up: A modular foundation for higher-order concurrent separation logic.

Ralf Jung, Robbert Krebbers, Jacques-Henri Jourdan, Ales Bizjak, Lars Birkedal, Derek Dreyer

J. Funct. Program., 2018

ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency.

Dan Frumin, Robbert Krebbers, Lars Birkedal

Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017

Interactive proofs in higher-order concurrent separation logic.

Robbert Krebbers, Amin Timany, Lars Birkedal

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

The Essence of Higher-Order Concurrent Separation Logic.

Robbert Krebbers, Ralf Jung, Ales Bizjak, Jacques-Henri Jourdan, Derek Dreyer, Lars Birkedal

Proceedings of the Programming Languages and Systems, 2017

2016

A Formal C Memory Model for Separation Logic.

Robbert Krebbers

J. Autom. Reason., 2016

Higher-order ghost state.

Ralf Jung, Robbert Krebbers, Lars Birkedal, Derek Dreyer

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq.

Robbert Krebbers, Louis Parlant, Alexandra Silva

Proceedings of the Theory and Practice of Formal Methods, 2016

2015

A Typed C11 Semantics for Interactive Theorem Proving.

Robbert Krebbers, Freek Wiedijk

Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014

Separation Algebras for C Verification in Coq.

Robbert Krebbers

Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

An operational and axiomatic semantics for non-determinism and sequence points in C.

Robbert Krebbers

Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Formal C Semantics: CompCert and the C Standard.

Robbert Krebbers, Xavier Leroy, Freek Wiedijk

Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013

The <i>λ</i><i>μ</i>^<i>T</i>-calculus.

Herman Geuvers, Robbert Krebbers, James McKinna

Ann. Pure Appl. Log., 2013

Separation Logic for Non-local Control Flow and Block Scope Variables.

Robbert Krebbers, Freek Wiedijk

Proceedings of the Foundations of Software Science and Computation Structures, 2013

Aliasing Restrictions of C11 Formalized in Coq.

Robbert Krebbers

Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012

A call-by-value lambda-calculus with lists and control

Robbert Krebbers

Proceedings of the Proceedings Fourth Workshop on Classical Logic and Computation, 2012

The lambda-mu-T-calculus

Herman Geuvers, Robbert Krebbers, James McKinna

CoRR, 2012

2011

The correctness of Newman's typability algorithm and some of its extensions.

Herman Geuvers, Robbert Krebbers

Theor. Comput. Sci., 2011

Type classes for efficient exact real arithmetic in Coq

Robbert Krebbers, Bas Spitters

Log. Methods Comput. Sci., 2011

A Formalization of the C99 Standard in HOL, Isabelle and Coq.

Robbert Krebbers, Freek Wiedijk

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Computer Certified Efficient Exact Reals in Coq.

Robbert Krebbers, Bas Spitters

Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

2010

Pure Type Systems without Explicit Contexts

Herman Geuvers, Robbert Krebbers, James McKinna, Freek Wiedijk

Proceedings of the Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2010