Ph. D. Study Plan
Noah Torp-Smith The IT University of Copenhagen September, 2004
Student Noah Torp-Smith, CPR: (Omitted in web-version) IT University of Copenhagen Department of Theoretical Computer Science Rued Langgaards Vej 7, DK-2300 Copenhagen S, Denmark Phone: +45 7218 5288, e-mail: noah@itu.dk Project: Reasoning about Resources Admission: August 1st, 2001 Submission of thesis: July 31st, 2005 Supervisor Associate Professor Lars Birkedal IT University of Copenhagen Rued Langgaards Vej 7, DK-2300 Copenhagen S, Denmark Head of Department of Theoretical Computer Science Phone: +45 7218 5280, e-mail: birkedal@itu.dk
Preface
[September 2003] This is a revised study plan. The time schedule has been modified to conform with the deadlines for half year reports at the IT University. [March 2004] Publication list, talk list, plans for teaching updated. Time schedule modified slightly to become more realistic. [September 2004] Publication list updated, plan for teaching updated. Time schedule updated to include studies of reflexive graphs, data bastraction and modularity.
1
Project Description
Objective
Practical programming languages used in industry, such as C, traditionally provide explicit access to computational resources such as, for example, the memory of a computer. This approach provides relatively fine-grained control over resource consumption, but the drawback is that it is extremely error-prone, since a sufficient in-depth understanding of the semantics of resources in a programming context does not exist as of now. The goal of this project is to provide some of this knowledge.
Background
It is important to be able to reason about resources. One of the major applications is in program verification: a better comprehension of resources can be used to verify that a program (written in a language which provides control over computational resources) has certain properties. This is tightly connected to the subject of program logics: one needs to...