Abstract

Guaranteeing that system processes do not need more resources, in terms of execution time, memory space, energy consumption, etc, than the ones that they have at their disposal is one fundamental aspect of software reliability. I start by surveying some results that I have obtained in the field of implicit computational complexity by means of linear type systems and semantics interpretation techniques. Then, I explain how these and similar results can be exploited for formally reasoning about the resource consumption of high level programming languages. An important aspect towards this goal is to show a direct correspondence between the resource usage discipline of the high-level program and the one of the effectively compiled code on a real machine. I suggest how this can be achieved by extending some recent results about certified compilation. I then conclude by presenting some related research direction I want to follow.