  Amortized analysis is a program cost analysis technique for data structures
in which the cost of operations is specified in aggregate, under the assumption
of continued sequential use. Typically, amortized analyses are presented
inductively, in terms of finite sequences of operations. We give an alternative
coinductive formulation and prove that it is equivalent to the standard
inductive definition. We describe a classic amortized data structure, the
batched queue, and outline a coinductive proof of its amortized efficiency in
$\textbf{calf}$, a dependent type theory for cost analysis.
