Gareth Smith

Table of Contents

Gareth/tree image

Figure 1: Gareth in a tree

Research Associate

Department of Computing
Huxley Building
Imperial College London
180 Queens Gate


Since writing this page I've left Imperial. Probably the best place to see what I'm up to now is my personal site.


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. I have been working with Philippa Gardner and Sergio Maffeis on program reasoning for JavaScript, and am a founding member of the JSCert project.


A Trusted Mechanised JavaScript Specification POPL 2014
JavaScript is the most widely used web language for client-side applications. Whilst the development of JavaScript was initially just led by implementation, there is now increasing momentum behind the ECMA standardisation process. The time is ripe for a formal, mechanised specification of JavaScript, to clarify ambiguities in the ECMA standards, to serve as a trusted reference for high-level language compilation and JavaScript implementations, and to provide a platform for high-assurance proofs of language properties.
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

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 (VSTTE Theory 2010 and Extended Techreport)
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.


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.

Other stuff

I am a founder of the JSCert project, which provides a complete mechanised operational semantics for the JavaScript programming language, in Coq.

I wrote about Bookshelves for a world with Internets in it.

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.

Author: Gareth Smith

Created: 2015-08-29 Sat 22:03