My research interests are somewhat varied. I work on formalising properties of object-oriented and object-capability programming languages, specifically a property called effect parametricity. I am also interested in secure compilation and full abstraction properties and applying logical relations to prove them. Furthermore, I work on functional and dependently typed programming and programming languages. I have worked on a Haskell parsing library called grammar-combinators and have added instance arguments to the programming language/proof assistant Agda. I have also worked on information flow security, in particular a technique called secure multi-execution.