Mobile Resource Guarantees
(MRG, project IST-2001-33149)

WP1: virtual machine and cost model

27/2/2002: Kenneth's A virtual machine platform for resource-bounded computation, v1.3 (delivered as D1a)
19/9/2002: Lennart's Cost model, version 1.6 (delivered as D1b)
19/12/2002: Various Grail documents, including: core Grail; toy Grail; resource-bounded functional programming on the JVM and .NET; Grail manual; Grail and .NET; a proposal for lambda-Grail; Grail compiler and decompiler (delivered as D1d)
13/1/2003: Lennart's Collection of examples (delivered as D1f)
28/4/2003: Lennart, Kenneth and Ian: Grail: a functional form for imperative mobile code, submitted to the FGC workshop.

WP2: logic of resources for bytecode

05/07/2002: Olha's document: Size Abstraction and Bound Functions for lambda-Grail Cost Model
12/07/2002: Olha's document: Tentative Schema: Generating and Solving Grail Cost Assertions
12/08/2002: Olha's document: Recursive Resource Bounds for lambda-Grail
13/08/2002: Lennart's note on applying separation logics for proving heap size assertions Assertion Language using separation logics
14/08/2002: Martin's proposal Resource-aware program logic via code instrumentation
24/09/2002: Hans' memo on A Resource-aware Abadi-Leino Logic.
21/12/2002: Merged ALLogic and SepLogic memos, together with notes on Proof-Carrying Code approach, to turn it into Deliverable 2a (delivered)
21/12/2002: Separate document on Operational Semantics of Grail.
13/01/2003: Olha's working document (an appendix for D2a, on completeness of PCC Logic for heaps) Axiomatics of Computations and Generic Effects.
04/07/2003: Olha's working document Toy Grail Examples and Proof Sketches for Certificate Generation.
1/9/2003: The bytecode logic and appendix (delivered as D2a/D2b)
4/9/2003: Matthew's project on encoding Grail/jGrail semantics (delivered as D2f)
28/11/2003: Hans-Wolfgang's document on proof checking (delivered as D2c)
28/11/2003: Lennart's and Alberto's document on theorem proving (delivered as D2e)

WP3: high-level programming language

15/4/2002: Olha's documents Basic languages for resource-bounded computation researches: C++ vs ML and The "offset problem" and compiling polymorphism
09/01/2003: Olha's High level functional language for resource-bounded computation, v2.1.3 (corrected delivered version, D3a)
13/1/2003: Kenneth's document describing the compilation procedure from Camelot (the high-level language) to Grail, v1.2 (delivered as D3b)
1/9/2003: Nicholas's project on optimisation plus an addendum on heap optimisation (delivered as D3e)
28/11/2003: Nicholas's document on O'Camelot (delivered as D3d)
19/02/2004: Stephen's Incorporating mutable state and concurrency into the high-level language (delivered as D3f)

WP4, WP5, WP7: resource-aware type systems

11/06/2002: Olha's document Resource Consumption Can be Evaluated by Recursive Functions? V.1.0.
14/06/2002: Olha's (Power Point) overview Existing Cost Models: Brief Classification and Some References. (pdf version)
The document conatines two schemata and a list of references. The first schema is an attempt to classify existing methods of resource consumption evaluation. The second one complements the first one and reflects different approaches to type annotations. The list of references containes short comments about the corresponding papers. All the papers are available via internet.
3/8/2002: Paper by Steffen (Jost) and Martin on Static Prediction of heap-space usage for first-order functional programs
22/08/2002: Hans' survey on papers relevant for WPs 2 and 4, especially resource-aware program logic and inference of resource bounds. (Survey in html,References in html).
10/12/2002: Roberto's Max-plus quasi-interpretations paper (delivered as D4a with this cover page)
19/11/2003: Kenneth's document about diamonds in Camelot, with full details (delivered as D4b and D4c)

WP6: generation of certificates

WP8: integration with existing security model

WP9: reducing size of certificates

WP10: mobile virtual machines

30/5/2003: Lennart and Stephen's Practical effectiveness of mobile virtual machines (delivered as D10a)
20/2/2004: Stephen's A metalanguage for Virtual Machines (delivered as D10b)

WP11: project management

23/6/2002: Don's Dissemination and use plan, v1.0 (delivered as D11j).
26/8/2002: Don's Self evaluation plan, v1.0 (delivered as D11f).
14/1/2003: Don's year 1 assessment of progress, v1.0 (delivered as D11g).
14/1/2003: First annual report, v1.0 (delivered)
3/3/2003: Reviewers' report on first review and cover letter
23/2/2004: Year two assessment of progress, v1.0 (delivered as D11h)
23/2/2004: Second annual report, v1.0 (delivered)
22/3/2004: Reviewers' report on second review (including cover letter)
8/10/2004: New Technical Annex with revised workplan
18/3/2005: Final assessment of progress (draft delivered as D11i)
18/3/2005: Third annual report (delivered)
18/3/2005: Report on 4-month extension (draft delivered)
3/5/2005: Reviewers' report on final review and cover letter

MRG overview material

23/5/2002: Lennart's MRG poster for Informatics Jamboree (superseded by NeSC poster, see below)
22/11/2002: MRG poster for e-Science Centre
23/1/2003: Paragraph describing MRG for Informatics publicity
24/3/2003: 300-word description of MRG for NeSC project list
24/7/2003: Lennart's summary of the ReQueST proposal for inclusion in a NeSC flyer, and their Powerpoint version
14/8/2003: Leaflet about MRG for handing to visitors etc., based on NeSC summary above
7/10/2004: Mobile Resource Guarantees for Smart Devices, for the CASSIS proceedings
29/4/2005: Summary about PCC and MRG, for Don's trip to Japan in June 2005, and the same thing (I hope) in Japanese. And an improved html-ised version.

GC and GC2 initiatives

26/3/2003: a vision for a GC2 pro-active initiative
26/3/2003: David Pearce's report on the GC initiative following the first review meetings
28/11/2003: GC2: text to be published in the official 2005 FP6 workprogramme and terms of reference, giving more details
25/5/2004: Kurt Geihs's report on the GC initiative following the second review meetings

Grant proposals

10/10/2002: Don's EPSRC application for a visiting fellowship for Zoltán Horváth
24/4/2003: ReQueST project proposal
28/1/2004: EmBounded project proposal
22/9/2004: MOBIUS project proposal
22/9/2004: FOG Network of Excellence proposal
23/10/2004: ReQueST project proposal (resubmission)

Miscellaneous

4/10/2001: Advert for MRG researchers
12/2/2002: Advert for summer students under the LFCS Summer Studentships scheme
15/5/2002: Proposals for student projects at Edinburgh: for MSc in 2002, for undergraduates in 2002/2003, for MSc in 2003
5/11/2002: submissions to MRG logo competition

External papers

12/3/2002: Paper (in French) from Gemplus Software Research about control of resources in smart cards
1/4/2002: Dave MacQueen. Should ML be object-oriented? Formal Aspects of Computing, 13:214-232 (2002). Includes a useful overview of approaches to adding objects to a functional language.
14/10/2002: Masters Thesis (in French) by Mathieu Baudet, done at Gemplus Software Research, on Contrôle de ressource et évitement des interblocages sur la mémoire