Separation Logic for Sequential Programs (Functional Pearl)

on YouTube ↗13m

" summary

A mechanized formalization claims a teachable Separation Logic for sequential programs with all definitions and proofs encoded in Coq formalization and material split into 10 chapters. It builds weakest preconditions, a ramified frame rule that avoids computing frame differences, a mix of affine and linear predicates, and a frame-friendly loop rule that simulates recursive reasoning for while loops. The lambda-calculus setup removes mutable-variable side conditions, simplifies proofs, and targets reuse in practical tooling; Coq and HTML sources are available.

AI-written summary · about

" chapters (13)

1. 0:00Intro
2. 0:27Contributions
3. 1:16Chapters of the course
4. 1:57Deep embedding of an imperative A-calculus
5. 3:21Shallow embedding of Separation Logic
6. 3:52Total correctness triples
7. 4:50The ramified frame rule Frame rule: almost never applicable
8. 6:32Weakest-precondition presentation Like in Hoare Logic, WP is a key ingredient for building practical tools. What definition for WP in SL? What frame rule in WP-style?
9. 8:04Mixing affine and linear predicates: motivation
10. 8:59(3) Mixing affine and linear predicates: a solution Definitions affine heaps
11. 10:12Frame-friendly rule for loops: motivation
12. 11:33(4) Frame-friendly rule for loops: solution Big-step specification state at the i-th iteration
13. 12:33Conclusion