About me

I will serve on the program committee for Interactive Theorem Proving (ITP).

I organised a workshop for HOL4 users, hosted at Arm.

I submitted to the Journal of Automated Reasoning (JAR) with other CakeML developers.

I served on the program committee for Interactive Theorem Proving (ITP).

I am working with Anthony Fox and Magnus Myreen (on sabbatical from Chalmers University of Technology).

I submitted to European Symposium on Programming (ESOP) with other PureCake developers. This won a distinguished artifact award, and was nominated for an ETAPS best paper award.

I successfully defended my thesis, subject to minor corrections. My external examiner/opponent was Xavier Leroy.

I submitted to Programming Language Design and Implementation Programming (PLDI) with other CakeML developers – see here for an overview.

I worked with Marco Elver and Aleksandr Nogikh on the Kernel Dynamic Tools team in Munich, improving syzkaller fuzzing for filesystems.

I worked with Dulma Churchill in the Infer London team, improving Infer’s Pulse taint analysis.

I submitted to Interactive Theorem Proving (ITP), building on my Arm internship – see here for an overview.

I worked with Catherine Gasnier in the Hack London team, improving type-inference for Hack by generating constraints on method invocations.

I worked with Anthony Fox in the security research group, investigating the Sail language ecosystem and its applications in formal reasoning about the semantics of the Arm instruction set.

I placed second at Principles of Programming Languages (POPL) 2020. This involved three rounds: an extended abstract, a poster, and a presentation.

I submitted to the Journal of Automated Reasoning (JAR) with other CakeML developers – see here for an overview.