Pruning the Infinite, Example-Based Synthesis using Context-Sensitive E-Graph Saturation

Matteo Bertorotta

Example based program synthesis has the potential of synthesizing any program. However, behavioral equivalences across programs often result in redundant and inefficient exploration of the search space. In my thesis I try to address this challenge by directing the search towards programs that solve at least one example. Thereby I focus on programs that behave similarly to the one desired. To achieve this goal, I use E-graphs to represent the space of behavioral equivalences in the context of individual examples.

---

Previous: | A Grounded Theory Study of "How Interactive Theorem Prover Programmers Write Code"
Next: Maria Khakimova | Enhancing Agda's Error Messages with Hints