- Abstract:
-
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.
- Links To Paper
- 1st Link
- Bibtex format
- @InBook{EDI-INF-RR-1188,
- author = {
Donald Sannella
and Martin Hofmann
and David Aspinall
and Stephen Gilmore
and Ian Stark
and Lennart Beringer
and Hans-Wolfgang Loidl
and Kenneth MacKenzie
and Alberto Momigliano
and Olha Shkaravska
},
- title = {Mobile resource guarantees},
- book title = {Trends in Functional Programming},
- publisher = {Intellect},
- year = 2007,
- volume = {6},
- pages = {211-226},
- url = {http://homepages.inf.ed.ac.uk/dts/pub/mrg-summary.pdf},
- }
|
