Robbert Krebbers

List of research outcomes

This list is not complete and representing at the moment only items from zbMATH Open and arXiv. We are working on additional sources - please check back here soon!

Publication	Date of Publication	Type
Interactive and automated proofs in modal separation logic (invited talk)	2024-11-26	Paper
Semi-automated reasoning about non-determinism in C expressions Programming Languages and Systems	2023-11-24	Paper
scientific article; zbMATH DE number 7566072 (Why is no real title available?)	2022-08-02	Paper
scientific article; zbMATH DE number 7407781 (Why is no real title available?)	2021-10-08	Paper
Moessner's theorem: an exercise in coinductive reasoning in \textsc{Coq}	2021-05-20	Paper
scientific article; zbMATH DE number 7340561 (Why is no real title available?)	2021-04-27	Paper
ReLoC: a mechanised relational logic for fine-grained concurrency Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science	2021-01-20	Paper
Iris from the ground up: a modular foundation for higher-order concurrent separation logic Journal of Functional Programming	2019-02-20	Paper
A formal C memory model for separation logic Journal of Automated Reasoning	2018-02-01	Paper
Interactive proofs in higher-order concurrent separation logic Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages	2017-10-20	Paper
The essence of higher-order concurrent separation logic Programming Languages and Systems	2017-05-19	Paper
Higher-order ghost state Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming	2017-05-10	Paper
Aliasing restrictions of C11 formalized in Coq Certified Programs and Proofs	2015-01-13	Paper
An operational and axiomatic semantics for non-determinism and sequence points in C Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages	2014-04-10	Paper
The \(\lambda \mu^{\mathbf{T}}\)-calculus Annals of Pure and Applied Logic	2013-04-15	Paper
Type classes for efficient exact real arithmetic in \textsc{Coq}	2013-04-09	Paper
Separation logic for non-local control flow and block scope variables Lecture Notes in Computer Science	2013-03-18	Paper
Computer Certified Efficient Exact Reals in Coq Lecture Notes in Computer Science	2011-07-29	Paper
A formalization of the C99 standard in HOL, Isabelle and Coq Lecture Notes in Computer Science	2011-07-29	Paper
The correctness of Newman's typability algorithm and some of its extensions Theoretical Computer Science	2011-07-07	Paper

Research outcomes over time

This page was built for person: Robbert Krebbers