| Publication | Date of Publication | Type |
|---|
| Modular verification of intrusive list and tree data structures in separation logic | 2026-02-10 | Paper |
| 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?)
(available as arXiv preprint) | 2022-08-02 | 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?)
(available as arXiv preprint) | 2021-10-08 | 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 |
scientific article; zbMATH DE number 7340561 (Why is no real title available?)
(available as arXiv preprint) | 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}
(available as arXiv preprint) | 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 |
