Project evaluation paper: 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 proceedingChapter


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 Volume 6
PublisherIntellect Books
Number of pages16
ISBN (Print)9781841501765
Publication statusPublished - Jul 2007

Cite this