Separation-logic proofs of heap-manipulating programs require careful accounting of objects and pointers in memory. On paper, these proofs are often accompanied by heap-memory diagrams that help authors and readers track the evolution of the program’s abstract state. However, users of interactive theorem provers must instead work with plain-text notations that obscure object relationships.

In Sepviz, we imitate an intuitive diagrammatic notation commonly used in research and educational materials about separation logic, support animation across proof steps, and make it easy to port to new frameworks.

Diagrams are rare and hard to work with in programming and theorem-proving environments. Existing diagramming systems do not meet the practical needs of interactive, exploratory use, such as keeping diagrams understandable as they grow in size with limited screen space, or as they evolve as the user steps through the program or proof. My research seeks to develop an approach—compositional diagramming—that meets these needs. Diagrams are formed of independent parts composed in systematic ways reflecting the structure of the represented object, and the diagramming system compiles a higher-level description of the object to lower-level diagram components. Techniques that make diagrams more practical, such as wrapping, folding, and packing, fit neatly into a compositional approach. Through my work, I hope to build a useful diagramming system for working computer scientists, mathematicians, and programmers, based on a better understanding of compositional diagrams.