I am a Principal Applied Scientist within the Automated Reasoning Group at Amazon Web Services, Cambridge, UK (AWS, henceforth). Prior to moving to AWS I was:

My portrait
  • A (Senior, then Staff, before finally being promoted to) Principal Research Engineer within the Systems Group at Arm Research, Cambridge, UK from 2017–2022. My research there focussed on privacy-preserving computation, as evidenced by the Confidential Computing Consortium-adopted Veracruz project, a project which I initiated and thereafter acted as technical lead on. Moreover, I also had a hand in developing software verification flows which provided strong evidence for the correctness for low-level, security-critical firmware, central to the Arm Confidential Computing Architecture (“Arm CCA”). This is a Confidential Computing technology that will be deployed as a point-release for the Armv9-A architecture, and will eventually be found in hundreds of millions of devices worldwide.
  • A Postdoctoral Research Scientist (a “postdoc”), from 2012–2017, at the Computer Laboratory at the University of Cambridge. Here, I worked on Prof. Peter Sewell’s Rigorous Engineering for Mainstream Systems (“REMS”) project. I helped develop the Lem specification language, and developed a formal semantics of ELF static linking. I also developed a side interest in the correctness of a class of distributed datastructure, called Conflict-free Replicated Datatypes (“CRDTs”).
  • A Postdoctoral Research Scientist (a “postdoc”), from 2010–2012, at the Dipartimento di Scienze dell’Informazione at the Alma Mater Studiorum, Università di Bologna. I worked with Dr. Claudio Sacerdoti Coen on the EU-funded Certified Complexity (“CerCo”) project, which aimed to produce a certified compiler, for a large fragment of C, capable of automatically lifting precise and reliable concrete complexity bounds from machine code to the original input source code. I worked on the implementation and verification of the CerCo C compiler backend, using the (now sadly defunct) Matita proof assistant.

I have a PhD in theoretical computer science from the Department of Mathematics and Computer Science at Heriot-Watt University, Edinburgh. I studied various topics at the intersection of nominal techniques, unification, and type-theory and lambda-calculi. My supervisors were Murdoch “Jamie” Gabbay and Phil Trinder.

Miscellanea

My Erdős Number is at most four: me ⇒ Gilles Dowek ⇒ Nachum Dershowitz ⇒ Andreas R. Blass ⇒ Paul Erdős.