This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Robbert Krebbers
A grouping.
The Iris line: higher-order concurrent separation logic as a framework rather than as a logic. The corpus holds the proof mode that made Iris usable inside Coq, the framework itself in 'Iris from the ground up', and RustBelt, its best-known application -- a semantic soundness proof for Rust's type system including the unsafe libraries underneath it.
3 references
Iris from the ground up: A modular foundation for higher-order concurrent separation logic
Ralf Jung and others (2018) · Journal of Functional Programming · Cambridge University Press
RustBelt: Securing the foundations of the Rust programming language
Ralf Jung and others (2018) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery
Interactive proofs in higher-order concurrent separation logic
Robbert Krebbers and others (2017) · 44th ACM Symposium on Principles of Programming Languages (POPL)