BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Talks.cam//talks.cam.ac.uk//
X-WR-CALNAME:Talks.cam
BEGIN:VEVENT
SUMMARY:Towards Automatic Resource Consumption Certification - Marco Gaboa
 rdi\, University of Bologna
DTSTART:20101105T110000Z
DTEND:20101105T120000Z
UID:TALK27837@talks.cam.ac.uk
CONTACT:Bjarki Holm
DESCRIPTION:Guaranteeing that system processes do not need more resources\
 , in terms of execution time\, memory space\, energy consumption\, etc\, t
 han the ones that they have at their disposal is one fundamental aspect of
  software reliability. I start by surveying some results that I have obtai
 ned in the field of implicit computational complexity by means of linear t
 ype systems and semantics interpretation techniques. Then\, I explain how 
 these and similar results can be exploited for formally reasoning about th
 e resource consumption of high level programming languages. An important a
 spect towards this goal is to show a direct correspondence between the res
 ource usage discipline of the high-level program and the one of the effect
 ively compiled code on a real machine. I suggest how this can be achieved 
 by extending some recent results about certified compilation. I then concl
 ude by presenting some related research direction I want to follow. 
LOCATION:Room SS03\, Computer Laboratory\, William Gates Building
END:VEVENT
END:VCALENDAR