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.