Building Blocks for Step-Indexed Program Logics

on YouTube ↗22m

" summary

Claims a single modular physical-step modality lets program-logic designers recover every prior multiple-later elimination technique without redoing metatheory, integrating with Iris and mechanized in Rocq. It migrates Actris, RefinedRust, Perennial and Trillium to the new brick while keeping the same user-facing WP rules, lets clients pick a step-count function f (only constraint f(0)=0), and provides adequacy proofs and artifacts (doi:10.1145/3779031.3779095, doi:10.5281/zenodo.17809073) so existing proofs can be reused.

AI-written summary · about

" chapters (14)

1. 0:00Step-indexed program logics intro
2. 1:25Why step indexing is needed
3. 3:10Later elimination problem
4. 4:32Multiple later elimination challenges
5. 6:37Iris separation logic overview
6. 8:45Approaches to multiple later elimination
7. 11:54Problems with current methods
8. 12:36Physical step update modality
9. 14:42Simplifying proofs with new block
10. 15:44Verifying across Iris projects
11. 16:27User choice in elimination
12. 17:10Parameterizing rules with f
13. 18:32Conclusion and future work
14. 19:38Q&A