I'm an RSDE in the Programming Principles and Tools group at Microsoft Research Cambridge, working on the SLAyer and TERMINATOR projects. I joined MSR in April 2008.

I worked for ARM 2000-2008 in the modelling and CPU verification group. I developed special purpose compilers/simulators, Random Instruction Sequence generators, Debug/Trace comparators, the AMBA bus protocol checker, and lots of ARM assembler tests that ran on bare metal.

I have an MEng from Imperial and a PhD in dependent type theory from Queen Mary. I was an RA on the original Verifiied Bytecode project.