Lennart Beringer, Kenneth MacKenzie and Ian Stark
In Foundations of Global Computing: Proceedings of the 2nd EATCS Workshop, Eindhoven, The Netherlands, 28-29 June 2003, Electronic Notes in Theoretical Computer Science 85.1. Elsevier, 2003.
Fetch paper (PDF, 342k). Go to other papers, talks or home page.
In Robert Louis Stevenson's novel [1], Dr Jekyll is a well-regarded member of polite society, while his alter ego Mr Hyde shares the same physical form but roams abroad communing with the lowest elements. In this paper we present Grail, a well-behaved first-order functional language that is the target for an ML-like compiler; while also being a wholly imperative language of assignments that travels and executes as Java classfiles. We use this dual identity in the Mobile Resource Guarantees project, where Grail serves as proof-carrying code to provide assurances of time and space performance, thereby supporting secure and reliable global computing.
[1] Robert Louis Stevenson. Strange Case of Dr. Jekyll and Mr. Hyde. Longmans, Green & Co., London, 1886.
@InProceedings{beringer/mackenzie/stark:graffi,
author = {Beringer and MacKenzie and Stark},
title = {Grail: a Functional Form for Imperative Mobile Code},
booktitle = {Foundations of Global Computing: Proceedings of the
2nd~EATCS Workshop},
year = 2003,
series = {Electronic Notes in Theoretical Computer Science},
number = {85.1},
publisher = {Elsevier},
month = jun,
url = {http://www.inf.ed.ac.uk/~stark/graffi.html},
pdf = {http://www.inf.ed.ac.uk/~stark/graffi.pdf}
}