Robbert Krebbers

Orcid: 0000-0002-1185-5237

Affiliations:
  • Radboud University Nijmegen, The Netherlands


According to our database1, Robbert Krebbers authored at least 53 papers between 2010 and 2024.

Collaborative distances:
  • Dijkstra number2 of four.
  • Erdős number3 of four.

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Deadlock-Free Separation Logic: Linearity Yields Progress for Dependent Higher-Order Message Passing.
Proc. ACM Program. Lang., January, 2024

Unification for Subformula Linking under Quantifiers.
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).
Proc. ACM Program. Lang., August, 2023

Proof Automation for Linearizability in Separation Logic.
Proc. ACM Program. Lang., April, 2023

DimSum: A Decentralized Approach to Multi-language Semantics and Verification.
Proc. ACM Program. Lang., January, 2023

Beyond Backtracking: Connections in Fine-Grained Concurrent Separation Logic.
Proc. ACM Program. Lang., 2023

Interactive and Automated Proofs in Modal Separation Logic (Invited Talk).
Proceedings of the 14th International Conference on Interactive Theorem Proving, 2023

2022
Later credits: resourceful reasoning for the later modality.
Proc. ACM Program. Lang., 2022

VIP: verifying real-world C idioms with integer-pointer casts.
Proc. ACM Program. Lang., 2022

Multiparty GV: functional multiparty session types with certified deadlock freedom.
Proc. ACM Program. Lang., 2022

Connectivity graphs: a method for proving deadlock freedom based on separation logic.
Proc. ACM Program. Lang., 2022

Simuliris: a separation logic framework for verifying concurrent program optimizations.
Proc. ACM Program. Lang., 2022

Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic.
Log. Methods Comput. Sci., 2022

Diaframe: automated verification of fine-grained concurrent programs in Iris.
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.
Proc. ACM Program. Lang., 2021

ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity.
Log. Methods Comput. Sci., 2021

Safe systems programming in Rust.
Commun. ACM, 2021

Compositional Non-Interference for Fine-Grained Concurrent Programs.
Proceedings of the 42nd IEEE Symposium on Security and Privacy, 2021

Transfinite Iris: resolving an existential dilemma of step-indexed separation logic.
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.
Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Machine-checked semantic session typing.
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.
Proc. ACM Program. Lang., 2020

Actris: session-type based reasoning in separation logic.
Proc. ACM Program. Lang., 2020

Scala step-by-step: soundness for DOT with step-indexed logical relations in Iris.
Proc. ACM Program. Lang., 2020

Intrinsically-typed definitional interpreters for linear, session-typed languages.
Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2020

2019
Iron: managing obligations in higher-order concurrent separation logic.
Proc. ACM Program. Lang., 2019

A benchmark for C program verification.
CoRR, 2019

Semi-automated Reasoning About Non-determinism in C Expressions.
Proceedings of the Programming Languages and Systems, 2019

2018
Intrinsically-typed definitional interpreters for imperative languages.
Proc. ACM Program. Lang., 2018

MoSeL: a general, extensible modal framework for interactive proofs in separation logic.
Proc. ACM Program. Lang., 2018

Mtac2: typed tactics for backward reasoning in Coq.
Proc. ACM Program. Lang., 2018

RustBelt: securing the foundations of the rust programming language.
Proc. ACM Program. Lang., 2018

Iris from the ground up: A modular foundation for higher-order concurrent separation logic.
J. Funct. Program., 2018

ReLoC: A Mechanised Relational Logic for Fine-Grained Concurrency.
Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, 2018

2017
Interactive proofs in higher-order concurrent separation logic.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

The Essence of Higher-Order Concurrent Separation Logic.
Proceedings of the Programming Languages and Systems, 2017

2016
A Formal C Memory Model for Separation Logic.
J. Autom. Reason., 2016

Higher-order ghost state.
Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Moessner's Theorem: An Exercise in Coinductive Reasoning in Coq.
Proceedings of the Theory and Practice of Formal Methods, 2016

2015
A Typed C11 Semantics for Interactive Theorem Proving.
Proceedings of the 2015 Conference on Certified Programs and Proofs, 2015

2014
Separation Algebras for C Verification in Coq.
Proceedings of the Verified Software: Theories, Tools and Experiments, 2014

An operational and axiomatic semantics for non-determinism and sequence points in C.
Proceedings of the 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014

Formal C Semantics: CompCert and the C Standard.
Proceedings of the Interactive Theorem Proving - 5th International Conference, 2014

2013
The <i>λ</i><i>μ</i><sup><i>T</i></sup>-calculus.
Ann. Pure Appl. Log., 2013

Separation Logic for Non-local Control Flow and Block Scope Variables.
Proceedings of the Foundations of Software Science and Computation Structures, 2013

Aliasing Restrictions of C11 Formalized in Coq.
Proceedings of the Certified Programs and Proofs - Third International Conference, 2013

2012
A call-by-value lambda-calculus with lists and control
Proceedings of the Proceedings Fourth Workshop on Classical Logic and Computation, 2012

The lambda-mu-T-calculus
CoRR, 2012

2011
The correctness of Newman's typability algorithm and some of its extensions.
Theor. Comput. Sci., 2011

Type classes for efficient exact real arithmetic in Coq
Log. Methods Comput. Sci., 2011

A Formalization of the C99 Standard in HOL, Isabelle and Coq.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

Computer Certified Efficient Exact Reals in Coq.
Proceedings of the Intelligent Computer Mathematics - 18th Symposium, 2011

2010
Pure Type Systems without Explicit Contexts
Proceedings of the Proceedings 5th International Workshop on Logical Frameworks and Meta-languages: Theory and Practice, 2010


  Loading...