Iowa Type Theory Commute

Separation Logic II: recursive predicates

Aaron Stump Season 3 Episode 35

Use Left/Right to seek, Home/End to jump to start or end. Hold shift to jump forward or backward.

0:00 | 11:52

I discuss separation logic basics some more, as presented in the seminal paper by John C. Reynolds.  An important idea is describing data structure using separating conjunction and recursive predicates.