The Logical Essence of Well-Bracketed Control Flow
summary
First Hoare-style separation logic for well-bracketed control flow that proves the closure-from-example always returns one when called with a function that preserves stack discipline; it introduces ghost stacks as a resource algebra that forces push/pop discipline, formalizes well-bracketed Hoare triples, derives unary and binary logical relations (sequential vs. concurrent variants), uses Iris as the meta-logic, and is mechanized in Coq with reusable artifacts available.
AI-written summary · about
chapters (8)
- 0:00Well-bracketed control flow intro
- 1:04Example program with refs/closures
- 2:50Limitations of program logics
- 4:33Ghost stacks for reasoning
- 8:11Proof outline with ghost stacks
- 11:45Logical relations for concurrency
- 12:48Conclusion and future work
- 13:09Q&A
related talks
20mHyper Hoare Logic: (Dis-)Proving Program Hyperproperties
15mHandling Bidirectional Control Flow
25mA Relational Separation Logic for Effect Handlers
01h 05mControl Flow Obfuscation for Featherweight Java + Efficient Fair Conjunction
16mS4 modal sequent calculus as intermediate logic and intermediate language (Short Paper)
22mImplementing separation logic using an SMT-backed Frame Rule
16mBeyond Relooper: Recursive Translation of Unstructured Control Flow to Structu…
17mCalculational design of Incorrectness Separation Logic