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.

Ralf Jung

A grouping.

Higher-order concurrent separation logic: the Iris framework, and the type-system soundness proofs built with it. Best known here for RustBelt, which proves Rust's ownership discipline sound including its unsafe core. Homepage: https://research.ralfj.de/

3 references

Completeness of Iris-Based Program Logics
Johannes Hostert and others (2026) · Proceedings of the ACM on Programming Languages · Association for Computing Machinery (ACM)
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