Sepviz examples

The following are demos of interactive literate proof scripts for separation-logic proofs covering different frameworks and data structures:

Using CFML: queues (queue transfer), binary trees (tree rotations), linked lists (list API)
Using Iris: queues (queue transfer, same proof as the CFML one) and linked lists (adapted from the Iris tutorial; uses iterated separating conjunction)
Using the variant of CFML in Separation Logic Foundations, part of the Software Foundations textbook series: the "Representation predicates" chapter (lists, list segments, stacks; visualizing trees is left as an exercise for the reader).