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.

Wed 15 Apr

14:00 - 16:00: ESOP - Session 5 at Skeel
Chair(s): Jan VitekNortheastern University
esop-2015-papers142909920000014:00 - 14:30
Burke FetscherNorthwestern University, Koen ClaessenChalmers University of Technology, Michał PałkaChalmers University of Technology, John HughesChalmers University of Technology, Robby FindlerNorthwestern University
esop-2015-papers142910100000014:30 - 15:00
Ezgi ÇiçekMPI-SWS, Deepak GargMPI-SWS, Umut AcarCarnegie Mellon University
esop-2015-papers142910280000015:00 - 15:30
Jeremy G. SiekIndiana University, Michael M. VitousekIndiana University, Matteo CiminiIndiana University, Sam Tobin-HochstadtIndiana University, Ronald GarciaUniversity of British Columbia
esop-2015-papers142910460000015:30 - 16:00
Stefan Schulze FrielinghausTechnische Universität München, Michael PetterTechnische Universität München, Helmut SeidlTechnische Universität München