Grail: a functional form for imperative mobile code

Lennart Beringer, Kenneth MacKenzie, Ian Stark

Research output: Contribution to journalArticlepeer-review

Abstract / Description of output

In Robert Louis Stevenson's novel[31], 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. This work was performed as part of the Mobile Resource Guarantees project, funded by the European Commission under the Fifth Framework's proactive initiative on Global Computing, IST-2001-33149. In addition, Ian Stark is funded by an EPSRC Advanced Research Fellowship in Mathematical Models for Concurrent and Mobile Computation, GR/R76950/01. We would like to thank all MRG members for the numerous discussions on Grail and Nicholas Wolverson for his help with the implementation of the compilers.
Original languageEnglish
Pages (from-to)3-23
Number of pages21
JournalElectronic Notes in Theoretical Computer Science
Volume85
Issue number1
DOIs
Publication statusPublished - 2003

Fingerprint

Dive into the research topics of 'Grail: a functional form for imperative mobile code'. Together they form a unique fingerprint.

Cite this