Recursive Program Synthesis using Paramorphisms
Qiantan Hong, Alex Aiken
Abstract
We show that synthesizing recursive functional programs using a class of primitive recursive combinators is both simpler and solves more benchmarks from the literature than previously proposed approaches. Our method synthesizes paramorphisms, a class of programs that includes the most common recursive programming patterns on algebraic data types. The crux of our approach is to split the synthesis problem into two parts: a multi-hole template that fixes the recursive structure, and a search for non-recursive program fragments to fill the template holes.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext bb8d78e2-5ba6-4121-b815-b2d1a66a0720Cited by top-tier papers2
- Programming By Scaffolded Demonstration with PerpendAngela Bi, Eric Rawn, Justin Lubin, Sarah E. ChasinsCHI 2026 · 2 citations
- The Search for Constrained Random GeneratorsHarrison Goldstein, Hila Peleg, Cassia Torczon, Daniel Sainati et al.PLDI 2026 · 1 citation
Builds on5
- Bottom-up synthesis of recursive functional programs using angelic executionAnders Miltner, Adrian Trejo Nuñez, Ana Brendel, Swarat Chaudhuri et al.POPL 2022 · 38 citations
- Cyclic program synthesisShachar Itzhaky, Hila Peleg, Nadia Polikarpova, Reuben N. S. Rowe et al.PLDI 2021 · 26 citations
- Inductive Synthesis of Structurally Recursive Functional Programs from Non-recursive ExpressionsWoosuk Lee, Hangyeol ChoPOPL 2023 · 19 citations
- Trace-Guided Inductive Synthesis of Recursive Functional ProgramsYongwei Yuan, Arjun Radhakrishna, Roopsha SamantaPLDI 2023 · 17 citations
- Adaptive restarts for stochastic synthesisJason R. Koenig, Oded Padon, Alex AikenPLDI 2021 · 3 citations
Related papers
- Counterexample-Guided Partial Bounding for Recursive Function SynthesisAzadeh Farzan, Victor NicoletCAV 2021 · 13 citations
- Proving Functional Program Equivalence via Directed Lemma SynthesisYican Sun, Ruyi Ji, Jian Fang, Xuanlin Jiang et al.FM 2024 · 2 citations
- Phased synthesis of divide and conquer programsAzadeh Farzan, Victor NicoletPLDI 2021 · 11 citations
- Synthesis with Asymptotic Resource BoundsQinheping Hu, John Cyphert, Loris D'Antoni, Thomas W. RepsCAV 2021 · 5 citations
- Combining the top-down propagation and bottom-up enumeration for inductive program synthesisWoosuk LeePOPL 2021 · 34 citations
