We present a new approach for specifying and verifying resource utilization of higher-order functional programs that use lazy evaluation and memoization. In our approach, users can specify the desired resource bound as templates with numerical holes e.g. as steps ≤ ? ∗ size(l) + ? in the contracts of functions, as well as express invariants necessary for establishing the bounds that may possibly depend on the state of memoization. Our approach operates in two phases: first generating an instrumented first-order program that accurately models the higher-order control flow, and the effects of memoization on resources, using sets, algebraic datatypes, and mutual recursion, and then verifying the contracts of the first-order program by producing verification conditions (VCs) of the form exists-forall using an extended assume/guarantee reasoning. We use our approach to verify precise bounds on resources such as evaluation steps, and number of heap-allocated objects, on 17 challenging data structures and algorithms. Our benchmarks, comprising of 5K lines of functional Scala code, include lazy mergesort, Okasaki’s real- time queue and deque data structures that rely on aliasing of references to first-class functions; lazy data structures based on numerical representations such as the conqueue data structure of Scala’s data-parallel library, cyclic streams such as hamming number sequence, as well as dynamic programming algorithms like Levenstein distance, Viterbi algorithm, and packrat parsing. Our evaluations show that, when averaged over all benchmarks, the actual runtime resource consumption is at least 80% of the value inferred by our tool when estimating the number of evaluation steps, and is at least 88% for the number of heap-allocated objects.