Research

I am interested in using recent results in computer science theory to make real programming easier. In particular using resource reasoning to reason about web programs. Most recently, I have been working with Philippa Gardner and Sergio Maffeis on program reasoning for JavaScript.

Publications

Towards a Program Logic for JavaScript (POPL 2012, and Extended Techreport)

JavaScript has become the most widely used language for client-side web programming. The dynamic nature of JavaScript makes understanding its code notoriously difficult, leading to buggy programs and a lack of adequate static-analysis tools. We believe that logical reasoning has much to offer JavaScript: a simple description of program behaviour, a clear understanding of module boundaries, and the ability to verify security contracts.

We introduce a program logic for reasoning about a broad subset of JavaScript, including challenging features such as prototype inheritance and with. We adapt ideas from separation logic to provide tractable reasoning about JavaScript code: reasoning about easy programs is easy; reasoning about hard programs is possible. We prove a strong soundness result. All libraries written in our subset and proved correct with respect to their specifications will be well-behaved, even when called by arbitrary JavaScript code.

Local Reasoning About Web Programs (PhD Thesis)

Since 1990, the world wide web has evolved from a static collection of reference pages to a dynamic programming and application-hosting environment. At the core of this evolution is the programming language JavaScript and the XML update library DOM. Every modern web browser contains a DOM implementation which allows JavaScript programs to read and alter the web page that the user is currently viewing. JavaScript and DOM are extremely successful, and this success may be in part due to their highly dynamic and tightly integrated nature. However, this very nature hinders formal program analysis and tool development. Even the implementation independent specification that defines DOM is largely written in the English language, and not using any formal system.

While client-side web programming was once a simple discipline of form validation and interface trickery, it is fast becoming a far more serious business encompassing application development for the emerging ubiquitous cloud. As this evolution gains pace there is an increasing demand for client-side tool support of the sort commonly enjoyed by enterprise programmers, working in more easily analysed languages such as Java.

This thesis makes use of recent developments in program reasoning using context logic to provide the first formal, compositional specification for the Fundamental Interfaces of DOM Core Level 1. It presents both a big-step operational semantics for the necessary operations of the library and a context logic for reasoning about programs which use the library. Finally, it presents example programs that use the library and shows how context logic can be used to prove useful properties of those programs.

Resource Reasoning about Mashups (Technical Report)

The growing ``mashup'' phenomenon involves websites using scripting languages alongside data to create complex applications that integrate data and code from many sources. This leads to problems with reliability, as either sources change unaware that they have a dependency of a remote service, or clients of a service use resources that are accidentally exposed, or the dynamic nature of the scripting languages cause unexpected interactions. We show how resource reasoning can be used to construct provably fault free mashup programs, where services deliberately expose a subset of their data and code, and clients ensure the integration of components is sound.

DOM: Towards a Formal Specification (Plan-X 2008)
Local Hoare Reasoning about DOM (PODS 2008)

The W3C Document Object Model (DOM) specifies an XML update library. DOM is written in English, and is therefore not compositional and not complete. We provide a first step towards a compositional specification of DOM. Unlike DOM, we are able to work with a minimal set of commands and obtain a complete reasoning for straight-line code. Our work transfers O'Hearn, Reynolds and Yang's local Hoare reasoning for analysing heaps to XML, viewing XML as an in-place memory store as does DOM. In particular, we apply recent work by Calcagno, Gardner and Zarfaty on local Hoare reasoning about simple tree update to this real-world DOM application. Our reasoning not only formally specifies a significant subset of DOM Core Level 1, but can also be used to verify, for example, invariant properties of simple JavaScript programs.

Talks

In January 2012, I presented my JavaScript work at several venues in the US. At Mozilla, the talk was recorded. You can watch that talk here, and follow along with the slides here.

About Me

I am a Research Associate working in Professor Philippa Gardner's group. You can find my CV here and my research interests and publication list above.

Models of Computation

The first part of the first assessed coursework for Models of Computation can be found here. You will need the source code here.

Other Stuff

I accidentally wrote a short guide to Getting Started with LaTeX.

I am the founder of the wombile project, which is a system designed to make it easy to produce a collaborative, location aware mobile experience using smartphones.