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
Times are displayed in time zone: Azores change

14:00 - 16:00
Session 5ESOP at Skeel
Chair(s): Jan VitekNortheastern University
14:00
30m
Talk
Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System
ESOP
Burke FetscherNorthwestern University, Koen ClaessenChalmers University of Technology, Michał PałkaChalmers University of Technology, John HughesChalmers University of Technology, Robby FindlerNorthwestern University
14:30
30m
Talk
Refinement Types for Incremental Computational Complexity
ESOP
Ezgi ÇiçekMPI-SWS, Deepak GargMPI-SWS, Umut A. AcarCarnegie Mellon University
15:00
30m
Talk
Monotonic References for Efficient Gradual Typing
ESOP
Jeremy G. SiekIndiana University, Michael M. VitousekIndiana University, Matteo CiminiIndiana University, Sam Tobin-HochstadtIndiana University, Ronald GarciaUniversity of British Columbia
15:30
30m
Talk
Inter-procedural Two-Variable Herbrand Equalities
ESOP
Stefan Schulze FrielinghausTechnische Universität München, Michael PetterTechnische Universität München, Helmut SeidlTechnische Universität München