April 10, 2013
Alejandro Serrano
Resource analysis aims to derive tight bounds on the usage of some numerical property. It is instrumental in a wide range of program transformations, including granularity control for parallel and distributed computing, and energy optimizations in embedded systems. In this talk we give an overview of the current state of the art in resource analysis, including the most widely used approaches to it: instrumented interpreters, potential method and recurrence posing. In many of these approaches a initial size analysis, which derives bounds on the size of terms in a program, is run. We look at size analysis using recurrences, the problems with this approach, and propose a solution in terms of sized types. Sized types allow to encode information about subterms in any position and depth, and gives raise to a more precise resource analysis.