Incremental computation aims to speed up re-runs of a program after
its inputs have been modified slightly. It works by recording a trace
of the program's first run and propagating changes through the trace
in incremental runs, trying to re-use as much of the original trace as
possible. The recent work CostIt is a type and effect system to
establish the time complexity of incremental runs of a program, as a
function of input changes. However, CostIt is limited in two
ways. First, it prohibits input changes that influence control
flow. This makes it impossible to type programs that, for instance,
branch on inputs that may change. Second, the soundness of CostIt
is proved relative to an abstract cost semantics, but it is unclear
how the semantics can be realized.

In this paper, we address both these limitations. We present DuCostIt,
a re-design of CostIt, that combines reasoning about costs of
change propagation and costs of from-scratch evaluation. The latter
lifts the restriction on control flow changes. To obtain the type
system, we refine Flow Caml, a type system for information flow
analysis, with cost effects. Additionally, we inherit from CostIt
index refinements to track data structure sizes and a co-monadic
type. Using a combination of binary and unary step-indexed logical
relations, we prove DuCostIt's cost analysis sound relative to not
only an abstract cost semantics, but also a concrete semantics, which
is obtained by translation to an ML-like language.