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

Displayed time zone: Azores change

14:00 - 16:00
Session 5ESOP at Skeel
Chair(s): Jan Vitek Northeastern University
14:00
30m
Talk
Making Random Judgments: Automatically Generating Well-Typed Terms from the Definition of a Type-System
ESOP
Burke Fetscher Northwestern University, Koen Claessen Chalmers University of Technology, Michał Pałka Chalmers University of Technology, John Hughes Chalmers University of Technology, Robert Bruce Findler Northwestern University
14:30
30m
Talk
Refinement Types for Incremental Computational Complexity
ESOP
Ezgi Çiçek MPI-SWS, Deepak Garg MPI-SWS, Umut A. Acar Carnegie Mellon University
15:00
30m
Talk
Monotonic References for Efficient Gradual Typing
ESOP
Jeremy G. Siek Indiana University, Michael M. Vitousek Indiana University, Matteo Cimini Indiana University, Sam Tobin-Hochstadt Indiana University, Ronald Garcia University of British Columbia
15:30
30m
Talk
Inter-procedural Two-Variable Herbrand Equalities
ESOP
Stefan Schulze Frielinghaus Technische Universität München, Michael Petter Technische Universität München, Helmut Seidl Technische Universität München