Research:
My research interests are in logic and semantics of computation. With John Reynolds (CMU) I developed separation logic, which addresses the problem of tractable reasoning about dynamically allocated objects. With David Pym (then at Queen Mary, now at Abereen) I developed bunched logic, a general logic of resource, which is a more abstract cousin of and precursor to separation logic. My concurrent separation logic (proven sound by Steve Brookes) has made inroads on the problem of modular reasoning about shared-memory concurrent programs.
In much of my work I have been interested in the concept of locality, the idea that programmers look at state in little pieces rather than keeping track of the entire global state. I proposed a connection between parametric polymorphism and local state in a JACM'95 paper with Bob Tennent. This spurred some of my later work on separation logic and the frame problem and what I called "local reasoning", that you can reason about a piece of code by talking only about the resources it touches instead of tracking the entire global state of a system. The local reasoning ideal remains challenging to achieve in practice, particularly for concurrent programs.
In recent years I've gotten involved in software tools research, particularly with the SpaceInvader team (Cristiano Calcagno, Dino Distefano, Hongseok Yang and I) in London and our SLAyer/TERMINATOR colleagues at Microsoft Cambridge (Josh Berdine, Byron Cook). The ideas on locality and separation eventually, after being married with abductive inference, allowed a certain kind of automatic program analysis to scale to millions lines of code, where previously only hundreds or a few thousands were possible (see new JACM paper above). Of late I've also been paying attention to some of the fascinatingly intricate fine-grained concurrent algorithms (Bornat, Rinetzky, Yang..). More generally, I have many excellent colleagues in the London/Cambridge area who are enthusiastically pursuing program logic and semantics, mechanized program verification and static program analysis; it is a great place for this sort of research at the moment.
Random Links (includes past and present):
CV
Publications
Resource Reasoning
TCS@QM
Separation Logic
Smallfoot
SpaceInvader
SLAyer
Terminator
East London Massive
Attack of the 50 Foot Spatial Dudes
Proof of Cyclic List Reversal