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 smaller independent parts composed in systematic ways reflecting the structure of the object being represented, 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. If successful, my work will result in a useful diagramming system for working computer scientists, mathematicians, and programmers, as well as in better theoretical understanding of the scope and limitations of compositional diagrams.

PhD student in computer science (PL/SE) at EPFL. Research interest: automatic diagramming to enrich our interfaces with programs and proofs. Follow me on Mastodon @shardulc@types.pl.

Diagrams are often compositional and structurally regular, just like the objects they represent, be it data structures, proof terms, algebraic objects, execution traces, or so on. Diagrams can compute and be computed with. Diagrams evolve systematically with steps of reasoning or execution. But our diagramming tools today don’t take advantage of any of this—we draw diagrams individually and ad hoc, letting go of the conceptual diagram the moment we have its concrete rendering. How might we instead specify a schema of diagrams, whose instances can be automatically created from the objects being represented? How might we treat diagrams as evolving computational objects separate from their renderings? How might we codify æsthetic preferences to make automatic diagrams also automatically pretty?