Grail: A functional form for imperative mobile code

Lennart Beringer, Kenneth MacKenzie, Ian Stark

Research output: Contribution to journalConference articlepeer-review

14 Scopus citations


In Robert Louis Stevenson's novel, 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 (US)
Pages (from-to)3-23
Number of pages21
JournalElectronic Notes in Theoretical Computer Science
Issue number1
StatePublished - Sep 2003
Externally publishedYes
EventFGC, Foundations of Global Computing , 2nd EATCS Workshop (Satellite Event of ICALP 2003) - Einhoven, Netherlands
Duration: Jun 28 2003Jun 29 2003

All Science Journal Classification (ASJC) codes

  • Theoretical Computer Science
  • General Computer Science


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

Cite this