ESOP 2015
Tue 14 - Thu 16 April 2015 London, United Kingdom
Wed 15 Apr 2015 14:30 - 15:00 at Skeel - Session 5 Chair(s): Jan Vitek

With recent advances, programs can be compiled to efficiently respond to incremental input changes. However, there is no language-level support for reasoning about the time complexity of incremental updates. Motivated by this gap, we present CostIt, a higher-order functional language with a lightweight refinement type system for compositionally proving upper bounds on incremental computation time. Type refinements specify which parts of inputs and outputs may change, as well as dynamic stability, a measure of time required to propagate changes to a program’s execution trace, given modified inputs. We prove our type system sound using a new step-indexed cost semantics for change propagation and demonstrate the precision and generality of our technique through examples.