Refinement Types for Incremental Computational Complexity

Abstract : 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.
Type de document :
Communication dans un congrès
24th European Symposium on Programming (ESOP), Apr 2015, London, United Kingdom. 9032, pp.406-431, <10.1007/978-3-662-46669-8_17>
Liste complète des métadonnées

https://hal.inria.fr/hal-01245888
Contributeur : Arthur Charguéraud <>
Soumis le : jeudi 17 décembre 2015 - 17:43:37
Dernière modification le : vendredi 18 décembre 2015 - 01:12:52

Identifiants

Collections

Citation

Ezgi Çiçek, Deepak Garg, Umut Acar. Refinement Types for Incremental Computational Complexity. 24th European Symposium on Programming (ESOP), Apr 2015, London, United Kingdom. 9032, pp.406-431, <10.1007/978-3-662-46669-8_17>. <hal-01245888>

Partager

Métriques

Consultations de la notice

57