file.pdf (497.81 kB)
Download file

Refinement Types for Incremental Computational Complexity

Download (497.81 kB)
journal contribution
posted on 01.01.1986, 00:00 authored by Ezgi Cicek, Deepak Garg, Umut A. Acar

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 proving asymptotic 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.


Publisher Statement

All Rights Reserved



Usage metrics