Types for Incremental Computational Complexity

execution time by re-using the trace of a prior execution of the
program intelligently. With recent advances, programs can be compiled
to their incremental versions automatically. However, thus far, there
is no language-level support for formally proving the time complexity
of incremental execution. Motivated by this gap, this talk presents
CostIt, a higher-order functional language equipped with a type theory
for proving asymptotic bounds on incremental computation time.  CostIt
uses type refinements to specify which parts of inputs and outputs may
change, as well as the program's incremental execution time. The talk
will cover the intuitions behind CostIt's design.