# Resource-Guided Program Synthesis

arXiv: https://arxiv.org/abs/1904.07415 · HTML: https://mlsanity.com/paper/1904.07415/

## Key facts

- Cited by 2 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 16 Apr 2019.

## Built on by (most cited first, 2 of 2)

- [Language-Based Agent Control](https://mlsanity.com/paper/2605.12863/) (2026)
- [SkillEffect: Checked Lowering for Memory-Bounded Agent Tools](https://mlsanity.com/paper/2608.17007/) (2026)

## Abstract (arXiv)

This article presents resource-guided synthesis, a technique for synthesizing recursive programs that satisfy both a functional specification and a symbolic resource bound. The technique is type-directed and rests upon a novel type system that combines polymorphic refinement types with potential annotations of automatic amortized resource analysis. The type system enables efficient constraint-based type checking and can express precise refinement-based resource bounds. The proof of type soundness shows that synthesized programs are correct by construction. By tightly integrating program exploration and type checking, the synthesizer can leverage the user-provided resource bound to guide the search, eagerly rejecting incomplete programs that consume too many resources. An implementation in the resource-guided synthesizer ReSyn is used to evaluate the technique on a range of recursive data structure manipulations. The experiments show that ReSyn synthesizes programs that are asymptotically more efficient than those generated by a resource-agnostic synthesizer. Moreover, synthesis with ReSyn is faster than a naive combination of synthesis and resource analysis. ReSyn is also able to generate implementations that have a constant resource consumption for fixed input sizes, which can be used to mitigate side-channel attacks.