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