University of Cambridge > Talks.cam > Logic and Semantics Seminar (Computer Laboratory) > Towards Automatic Resource Consumption Certification

Towards Automatic Resource Consumption Certification

Add to your list(s) Download to your calendar using vCal

If you have a question about this talk, please contact Bjarki Holm.

Note unusual time (11am) and room (SS03)

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.

This talk is part of the Logic and Semantics Seminar (Computer Laboratory) series.

Tell a friend about this talk:

This talk is included in these lists:

Note that ex-directory lists are not shown.

 

© 2006-2020 Talks.cam, University of Cambridge. Contact Us | Help and Documentation | Privacy and Publicity