@InProceedings{DiagrammaticNotations+HATRA23,
  author       = {Chiplunkar, Shardul and Pit-Claudel, Clément},
  title        = {Diagrammatic notations for interactive theorem proving},
  booktitle    = {4th International Workshop on Human Aspects of Types and Reasoning Assistants},
  year         = 2023,
  series       = {{HATRA} 2023},
  month        = oct,
  doi          = {10.5075/epfl-SYSTEMF-305144},
  location     = {Cascais, Portugal},
  numpages     = 10,
  abstract     = {Diagrams are ubiquitous in the development and presentation of proofs, yet surprisingly uncommon in computerized mathematics. Instead, authors and developers rely almost exclusively on line-oriented notations (textual abbreviations and symbols). How might we enrich interactive theorem provers with on-the-fly visual aids that are just as usable? We answer this question by identifying a key challenge: designing declarative languages for composable diagram templates, that provide good-looking implementations of common patterns, and allow for rapid prototyping of diagrams that remain stable across transformations and proof steps.}
}