Equivalence by Canonicalization for Synthesis-Backed Refactoring

Explore a 20-minute video presentation from PLDI 2024 introducing a novel enumerative program synthesis framework called component-based refactoring. Discover how this approach transforms 'direct' style code into equivalent 'combinator' style code using library components. Learn about the innovative equivalence by canonicalization technique for checking code equivalence without relying on input-output examples or logical specifications. Examine the framework's implementation in two contexts: higher-order functional combinators in Elm and high-performance numerical computing combinators in NumPy for Python. Gain insights into the performance and output quality of the Cobbler tool, which instantiates this framework. Understand how synthesis-backed refactoring can be applied across various domains without requiring additional specification beyond the input program.

[PLDI24] Equivalence by Canonicalization for Synthesis-Backed Refactoring