Grail
Grail: a functional form for imperative mobile code. In the novel by {it R. L. Stevenson} [The strange case of Dr. Jekyll and Mr. Hyde. London: Longmans, Green (1886)], 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.
Keywords for this software
References in zbMATH (referenced in 5 articles , 1 standard article )
Showing results 1 to 5 of 5.
Sorted by year (- Charguéraud, Arthur; Pottier, François: Verifying the correctness and amortized complexity of a union-find implementation in separation logic with time credits (2019)
- Jaghoori, Mohammad Mahdi; de Boer, Frank; Longuet, Delphine; Chothia, Tom; Sirjani, Marjan: Compositional schedulability analysis of real-time actor-based systems (2017)
- Aspinall, David; Beringer, Lennart; Hofmann, Martin; Loidl, Hans-Wolfgang; Momigliano, Alberto: A program logic for resources (2007)
- Beringer, Lennart; Hofmann, Martin; Momigliano, Alberto; Shkaravska, Olha: Automatic certification of heap consumption (2005)
- Beringer, Lennart; MacKenzie, Kenneth; Stark, Ian: Grail: a functional form for imperative mobile code (2003)