New

Structural Separation Logic - A presentation on a Hoare Reasoning for highly structured data, given at the Oxford Concurrency Workshop in July 2013
... Me forgetting to upload anything in this period
JavaDOM: A Java implemenation of Featherweight DOM. October 2009
Imperial DoC Mac Setup Guide: An unofficial guide for the setup of new Macs within the department. October 2009
Transfer Report: My first year transfer report. July 2009
ArboreDOM: A visualisation tool for DOM reasoning. July 2009
CDOM: A C implemenation of Featherweight DOM. May 2009

Projects

I'm currently spending most of my time working on either the Reasonable Web Language, or automation of program reasoning using Hoare techniques and "Context" logics. This is all under the sage supervision of Philippa Gardner.

Monographs & Presentations

I sometimes write a few pages on various subjects, to help crystallise my ideas in the area. These monographs are not peer reviewed, don't (necessarily) represent the ideas of our group, and are quite possibly full of errors. None the less, here they are, alongside various presentations I've given.

• Structural Separation Logic - A presentation on a Hoare Reasoning for highly structured data, given at the Oxford Concurrency Workshop in July 2013
• Turning theory into practice - Emprical data for justifying a theoritical approach
• Verification meets testing - How formal software verification will probably benefit from formal testing ideas
• The Spirit of JavaScript (Unfinished)

Publications

1. "Local Reasoning about Mashups". (with Gardner & Smith), VSTTE 2010 Theory workshop
2. "Local Reasoning for a Global Web". Masters Thesis, Imperial College, September 2008
3. "Verifying Web Programs via Local Reasoning". PhD Transfer Report

Experiments

The ArboreDOM is visualisation tool for reasoning about DOM programs. Why not watch a video explaining it?

CDOM is a C implementation of our Featherweight DOM concept, so we can compare the low and high level reasoning. Have a look.

Below are some random experiments that required a web browser.

• Closures in Javascript
• Block scoping in Javascript
• Array semantics of Javascript
• Javascript function reintroduction
• Array unset semantics of PHP

Contact details

My e-mail address is at the top of this page, along with my postal address. Group members who don't have my mobile phone number are welcome to e-mail me for it. My office is Huxley 433, but to ensure I'm there, you'd be wise to e-mail first.

My CV can be found (nowhere at the moment). I also keep an erratically updated weblog at http://www.archgrove.co.uk/.