Generically Automating Separation Logic by Functors, Homomorphisms, and Modules

on YouTube ↗20m

" summary

Claims a generic theory that generates separation logic reasoning rules from algebraic signatures (functors, homomorphisms, modules) and a compositional instantiation algorithm that builds concrete reasoners from those signatures. Implementation formalizes proofs and the framework in Isabelle/HOL and uses sledge hammer for SMT discharge. Experiments show automatically instantiated reasoners match bespoke systems on many benchmarks, fully automate most cases, and handle examples around 150 LOC where total proof time peaks near 6–10 minutes, exploiting functor distributivity.

AI-written summary · about

" chapters (11)

1. 0:00Introduction
2. 1:30Compositional challenges
3. 2:34Reasoning system overview
4. 3:39Separation logic predicates
5. 5:46Parametric predicates and functors
6. 7:55Program state specifications
7. 9:20Hierarchical reasoning
8. 10:43Distributivity in transformations
9. 13:20Composite predicate properties
10. 15:08Experimental results
11. 17:19Summary