by this gap, we equip a list-processing language with a cost-accounting
semantics and a type system for compositionally proving the
complexity of such updates. Our type system includes novel
refinements that bound changes to inputs and captures dynamic stability,
a measure of the time required to re-run a program, given the
trace of an earlier execution with boundedly different inputs. Effectively,
our type system proves a computational continuity property
that bounds not only output changes but also changes to the trace
as a function of input changes. We prove our type system sound
relative to the cost semantics and verify experimentally that the
cost semantics is realistic in practice.