Diagramming for programs and proofs

Event details
Date | 27.06.2023 |
Hour | 14:00 › 16:00 |
Speaker | Shardul Chiplunkar |
Location | |
Category | Conferences - Seminars |
EDIC candidacy exam
Exam president: Prof. Viktor Kuncak
Thesis advisor: Prof. Clément Pit-Claudel
Co-examiner: Prof. James Larus
Abstract
We consider the problem of automatic diagramming in the context of programming environments and proof assistants: specifying and automatically drawing diagrams representing objects, proofs, and processes from the underlying system. We present and evaluate three instances of related work. The first is a system for automatic mathematical diagramming based on DSL specification and numerical constraint solving [1]. The second is a functional program calculation approach to the classic problem of pretty printing [2]. The third is a diagrammatic notional machine for Prolog with corresponding software to generate such diagrams [3]. Drawing on the successes and limitations of these lines of research, we lay out our research vision for automatic diagramming: natural specifications of diagrams and diagrammatic computations that generate structurally regular, extensible, pretty diagrams.
Background papers
Exam president: Prof. Viktor Kuncak
Thesis advisor: Prof. Clément Pit-Claudel
Co-examiner: Prof. James Larus
Abstract
We consider the problem of automatic diagramming in the context of programming environments and proof assistants: specifying and automatically drawing diagrams representing objects, proofs, and processes from the underlying system. We present and evaluate three instances of related work. The first is a system for automatic mathematical diagramming based on DSL specification and numerical constraint solving [1]. The second is a functional program calculation approach to the classic problem of pretty printing [2]. The third is a diagrammatic notional machine for Prolog with corresponding software to generate such diagrams [3]. Drawing on the successes and limitations of these lines of research, we lay out our research vision for automatic diagramming: natural specifications of diagrams and diagrammatic computations that generate structurally regular, extensible, pretty diagrams.
Background papers
- Ye, Katherine and Wode Ni, Max Krieger, Dor Ma'ayan, Jenna Wise, Jonathan Aldrich, Joshua Sunshine, Keenan Crane. “Penrose: From mathematical notation to beautiful diagrams.” SIGGRAPH 2020. https://doi.org/10.1145/3386569.3392375
- Bernardy, Jean-Philippe. “A pretty but not greedy printer (functional pearl).” ICFP 2017. https://doi.org/10.1145/3110250
- Eisenstadt, Marc and Mike Brayshaw. “A fine-grained account of Prolog execution for teaching and debugging.” Instructional Science 1990. https://doi.org/10.1007/BF00116447
Practical information
- General public
- Free
Contact
- edic@epfl.ch