My current interests centre around formal program verification. I am currently investigating how to expand verification techniques making use of separation logic and cyclic proofs in the context of the Cyclist theorem proving framework. I am also interested in type systems and type-based analysis in general, with particular emphasis on intersection types and guarded recursive types.

My wider research interests also include: programming languages and language design (I am affiliated with the SLURP research group at Imperial College London); fundamental models of computation (Lambda Calculus, Term Rewriting Systems, Process Calculi); Curry-Howard Isomorphisms; Logics for Computer Science.

An older research interest, which has been on the back burner for a while, is in frameworks for extensible programming languages, and recursive adaptive grammars in particular.

Recent & Unpublished Work