Mobile Resource Guarantees

Donald Sannella, Martin Hofmann, David Aspinall, Stephen Gilmore, Ian Stark, Lennart Beringer, Hans-Wolfgang Loidl, Kenneth MacKenzie, Alberto Momigliano, Olha Shkaravska

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract / Description of output

The Mobile Resource Guarantees (MRG) project has developed a proof-carrying-code infrastructure for certifying resource bounds of mobile code. Key components of this infrastructure are a certifying compiler for a high-level language, a hierarchy of program logics, tailored for reasoning about resource consumption, and an embedding of the logics into a theorem prover. In this paper, we give an overview of the project's results, discuss the lessons learnt from it and introduce follow-up work in new projects that will build on these results.
Original languageEnglish
Title of host publicationTrends in Functional Programming
PublisherIntellect Books
Number of pages16
Publication statusPublished - 2007


Dive into the research topics of 'Mobile Resource Guarantees'. Together they form a unique fingerprint.

Cite this