Program synthesis is the machine-assisted construction of provably correct programs from formal high-level specifications. Automated synthesis tools appeared soon after the introduction of theorem provers in the 1960s and, owing to a revived interest in the field during the 1990s, have now matured to a state in which they are routinely used in projects outside of research laboratories. Despite this success, however, program synthesis remains challenged by broadening demands for program quality, as for the next generation of synthesis tools the main focus shifts from program correctness to program efficiency. This thesis introduces our approach to automated computational complexity analysis and certification of higher-order functional programs as a means to resource-conscious program synthesis. First, we develop a general framework for expressing higher-order computational complexity of functional programs. Our compositional calculus is based on complexity annotations of an open-ended operational semantics and defines the complexity of a function as the cost of reducing the function term applied to a symbolic argument. Higher-type arguments are assigned a canonical computational skeleton whose decomposition exposes their internal structure. Second, we present algorithms that automatically generate and solve parameterized higher-type recurrence equations expressing the complexity of recursive functions. The recurrence generator uses symbolic evaluation to derive equations for primitive and general recursive terms. The recurrence solver reduces these equations to systems of unparameterized first-order recurrence equations that can be solved by conventional methods. A collection of simplification heuristics eliminates intractable functions by approximation. Third, we formalize our calculus and automate the construction of formal proofs that assert the correctness of the symbolic evaluation result. Proofs use a basic term reflection mechanism to reason intensionally about term evaluation at the meta-level. The Automated Complexity Analysis System implementation demonstrates the viability of our approach. The system uses the Nuprl proof development system and the Mathematica computer algebra system to compute the time complexity of Nuprl proof extracts. It has been able to identify automatically infeasible synthesized code whose manual discovery had taken many days previously.