The Nextgen Modality: A Modality for Non-Frame-Preserving Updates in Separation Logic

This conference talk presents a novel "nextgen modality" that enables reasoning across generations where resources can be updated in non-local and non-frame-preserving ways within separation logic. Explore how researchers from Aarhus University extend the Iris base logic with this new capability, demonstrating that existing Iris modalities are special cases of their proposed nextgen modality. Learn how this approach generalizes and simplifies the Iris base logic while enabling practical applications, particularly in constructing a separation logic for programming languages with explicit stack allocation and stack frame clearing operations. The presentation showcases the first separation logic for a high-level programming language with stack allocation, with supplementary artifacts available through Zenodo. Delivered at the CPP 2025 conference sponsored by ACM SIGPLAN and ACM SIGLOG, this 22-minute talk offers valuable insights for researchers working with separation logic, Iris, Coq, and program logic.