Research Interests

I am interested in the application of theory and tools for the specification and verification of semi-structured and heap-based data update. I am also interested in type safe code generation.

News

3 Nov 2008. Final versions of two POPL09 papers, on compositional shape analysis and Classical BI, are available from the publications page.

2 Nov 2008. I will be on the PC of POPL 2010.

25 Sep 2008. SpaceInvader in THE press.

15 Sep 2008. I will be PC chair of the Symposium on Automatic Program Verification, APV 2009, Argentina, February 14-15, 2009.

16 Sep 2008. East London Massive has released SpaceInvader 1.0.

Software

Smallfoot: automatic verification in separation logic. The cousin SmallfootRG supports fine-grained concurrency. For news about Space Invader, see Dino’s Blog.

MetaOCaml: a multi-staged extension of OCaml.

Publications

Here is a complete list

Program Committees

+ POPL 2010

+ IWACO 2009

+ TOOLS 2009

+ APV 2009 (Chair)

+ LICS 2008

+ PEPM 2008

+ FOSSACS 2007

+ HAV 2007 (Heap Analysis and Verification)

+ GPCE 2005

+ MetaOCaml 2005

+ COSMICAH 2005

+ MetaOCaml 2004

+ SPACE 2004

Links

I am also a member of the East London Massive.