Ian Stark

Grail: a Functional Form for Imperative Mobile Code

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.

  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}

Page last modified: Sunday 26 January 2014