Robbert Krebbers

Available identifiers

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	2023-11-24	Paper
https://portal.mardi4nfdi.de/entity/Q5094146	2022-08-02	Paper
https://portal.mardi4nfdi.de/entity/Q5155670	2021-10-08	Paper
Moessner's theorem: an exercise in coinductive reasoning in \textsc{Coq}	2021-05-20	Paper
https://portal.mardi4nfdi.de/entity/Q4986734	2021-04-27	Paper
ReLoC: a mechanised relational logic for fine-grained concurrency	2021-01-20	Paper
Iris from the ground up: a modular foundation for higher-order concurrent separation logic	2019-02-20	Paper
A formal C memory model for separation logic	2018-02-01	Paper
Interactive proofs in higher-order concurrent separation logic	2017-10-20	Paper
The essence of higher-order concurrent separation logic	2017-05-19	Paper
Higher-order ghost state	2017-05-10	Paper
Aliasing restrictions of C11 formalized in Coq	2015-01-13	Paper
An operational and axiomatic semantics for non-determinism and sequence points in C	2014-04-10	Paper
The \(\lambda \mu^{\mathbf{T}}\)-calculus	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	2013-03-18	Paper
Computer Certified Efficient Exact Reals in Coq	2011-07-29	Paper
A formalization of the C99 standard in HOL, Isabelle and Coq	2011-07-29	Paper
The correctness of Newman's typability algorithm and some of its extensions	2011-07-07	Paper

This page was built for person: Robbert Krebbers