Diagramming for programs and proofs

Thumbnail

Event details

Date 27.06.2023
Hour 14:0016: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
  1. 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
  2. Bernardy, Jean-Philippe. “A pretty but not greedy printer (functional pearl).” ICFP 2017. https://doi.org/10.1145/3110250
  3. 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

Tags

EDIC candidacy exam

Share