Equivalence by Canonicalization for Synthesis-Backed Refactoring
We present an enumerative program synthesis framework called component-based refactoring that can refactor “direct” style code that does not use library components into equivalent “combinator” style code that does use library components. This framework introduces a sound but incomplete technique to check the equivalence of direct code and combinator code called equivalence by canonicalization that does not rely on input-output examples or logical specifications. Moreover, our approach can repurpose existing compiler optimizations, leveraging decades of research from the programming languages community. We instantiated our new synthesis framework in two contexts: (i) higher-order functional combinators such as map
and filter
in the statically-typed functional programming language Elm and (ii) high-performance numerical computing combinators provided by the NumPy library for Python. We implemented both instantiations in a tool called Cobbler and evaluated it on thousands of real programs to test the performance of the component-based refactoring framework in terms of execution time and output quality. Our work offers evidence that synthesis-backed refactoring can apply across a range of domains without specification beyond the input program.
Thu 27 JunDisplayed time zone: Windhoek change
10:40 - 12:20 | Grammars and Code and FormalismsPLDI Research Papers at Sweden Chair(s): Nadia Polikarpova University of California at San Diego | ||
10:40 20mTalk | Equivalence by Canonicalization for Synthesis-Backed Refactoring PLDI Research Papers Justin Lubin University of California at Berkeley, Jeremy Ferguson University of California-Berkeley, Kevin Ye University of California at Berkeley, Jacob Yim UC Berkeley, Sarah E. Chasins University of California at Berkeley DOI | ||
11:00 20mTalk | PL4XGL: A Programming Language Approach to Explainable Graph Learning PLDI Research Papers DOI | ||
11:20 20mTalk | Syntactic Code Search with Sequence-to-Tree Matching PLDI Research Papers Gabriel Matute UC Berkeley, Wode Ni Columbia University, Titus Barik Apple, Alvin Cheung University of California at Berkeley, Sarah E. Chasins University of California at Berkeley DOI | ||
11:40 20mTalk | V-Star: Learning Visibly Pushdown Grammars from Program Inputs PLDI Research Papers DOI | ||
12:00 20mTalk | Hashing Modulo Context-Sensitive Alpha-Equivalence PLDI Research Papers Lasse Blaauwbroek Czech Institute for Informatics Robotics and Cybernetics, Miroslav Olšák Institut des Hautes Études Scientifiques, Herman Geuvers Radboud University Nijmegen, Netherlands DOI Pre-print |