Reasoning About Client Side Web Programs

February 27, 2013
Gareth Smith | Imperial College London

In 1996, the first JavaScript interpreter was shipped with Netscape Navigator. Since then the web has become an application platform, and JavaScript has evolved into “the assembly language of the web”. There are now JavaScript implementations of word processors, spreadsheets, chat programs, image editors and FPS games. Unfortunately, writing large reliable software in JavaScript can be extremely challenging. JavaScript makes it difficult to write modular programs and is notorious for its corner cases, which are easy to trip over.

In the JSCert project (http://jscert.org) we have been working to provide a trusted semantics and program logic for client side web programming. Our goal is to make it possible to produce truly high confidence client-side web programs. This talk will present a program logic, based on separation logic, for client side web programming.

Speaker Details

Gareth Smith is a Research Associate working with Philippa Gardner at Imperial College London. His main interest is reasoning about web programming, JavaScript and DOM. Before Imperial he worked at BBC R&D, for a small web startup, and as an independent consultant. Among the projects he completed in these roles is a distributed mobile gaming platform used to study the social and collaborative behaviour of key demographics.