A typical way of analyzing the time complexity of functional programs is to
extract a recurrence expressing the running time of the program in terms of the
size of its input, and then to solve the recurrence to obtain a big-O bound.
For recurrence extraction to be compositional, it is also necessary to extract
recurrences for the size of outputs of helper functions. Previous work has
developed techniques for using logical relations to state a formal correctness
theorem for a general recurrence extraction translation: a program is bounded
by a recurrence when the operational cost is bounded by the extracted cost, and
the output value is bounded, according to a value bounding relation defined by
induction on types, by the extracted size. This previous work supports
higher-order functions by viewing recurrences as programs in a lambda-calculus,
or as mathematical entities in a denotational semantics thereof. In this
paper, we extend these techniques to support amortized analysis, where costs
are rearranged from one portion of a program to another to achieve more precise
bounds. We give an intermediate language in which programs can be annotated
according to the banker's method of amortized analysis; this language has an
affine type system to ensure credits are not spent more than once. We give a
recurrence extraction translation of this language into a recurrence language,
a simply-typed lambda-calculus with a cost type, and state and prove a bounding
logical relation expressing the correctness of this translation. The
recurrence language has a denotational semantics in preorders, and we use this
semantics to solve recurrences, e.g analyzing binary counters and splay trees.