Diagrammatic notations for interactive theorem proving
summary
Argues that interactive theorem provers need declarative diagram languages that match text macros by delivering low-cost composition and good-looking idioms; proposes a template language built from grid/box primitives, recursive bounding-box composition, connectors, transposition heuristics and canonical layout rules so diagrams remain stable as proofs step forward. Demonstrations use custom rendering code rather than a finished tool; next steps are language design, workflow integration with provers, continuity heuristics (replay/animation) and prototype implementations.
AI-written summary · about
chapters (10)
- 0:00Diagrammatic notations intro
- 1:07History of diagrammatic proofs
- 4:15Diagrams missing in proof assistants
- 7:50Five principles from text notations
- 11:25Structure-driven composition
- 13:51Idioms for diagrammatic notations
- 16:58Continuity in diagram systems
- 18:21Summary of principles
- 19:03Future research directions
- 20:10Q&A
related talks
39mDiagrams as Code 2.0
15mDraw me a software or the art of diagrams that stick in the mind
32mA Survey of Weak Reasoning Assistants
50mDesign Patterns for Software Diagramming
41mDesign Patterns for Software Diagramming
22mInducTeX: A MetaCoq plugin for typesetting inductive definitions
50mVisualise, Document & Explore Your Software Architecture
08mExample-driven development: bridging tests and documentation