Grail: A functional form for imperative mobile code

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.