My research interests are somewhat varied. Current topics:

• formalising properties of object-oriented and object-capability programming languages, specifically a property called effect parametricity.
• formal reasoning about capability machines (CPUs with a built-in form of low-level object capabilities).
• secure compilation and full abstraction properties and applying logical relations to prove them.
• functional and dependently typed programming and programming languages, particularly Agda and Haskell