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 HP) 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 recent years I've gotten involved in
tools research,
particularly with the SpaceInvader team (Cristiano Calcagno,
Dino Distefano, Hongseok Yang and me) in London
and our SLAyer/TERMINATOR colleagues at Microsoft Cambridge (Josh Berdine,
Byron Cook).
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.
