I’m a PhD candidate at the University of Cambridge, Department of Computer Science and Technology. My topic is Machine Learning for Automated Theorem Proving and I’m supervised by Prof. Larry Paulson and Dr. Sean Holden.

I’m hoping to improve first-order logic theorem provers by augmenting their heuristics with inference based on data from previous proof attempts.

Education

(2016 — 2020) PhD in Computer Science, University of Cambridge

Topic: Machine Learning for Automated Theorem Proving

(2014 — 2015) MPhil in Advanced Computer Science, University of Cambridge

Result: Distinction

(2003 — 2007) B.Sc (Hons) Computer Science with Industrial Experience, University of Manchester

Result: First Class Honours

Work Experience

(Jun 2020 — Sep 2020) Research Internship, Amazon Web Services

Bayesian Optimisation for strategy invention in MiniSat solver. Optimisation of solver backends in the Dafny prover.

(Sep 2019 — Nov 2019) Research Internship, Amazon Web Services

Optimisation of backend solver parameters in CBMC using bayesian optimisation.

(Aug 2015 — Nov 2015) Internship, Computer Lab, University of Cambridge

Prototyped a tool-chain to compile high-level hardware descriptions down to FPGAs.

(Apr 2011 — May 2014) Sofware Engineer, Intel Labs

Hardware-software co-designed microprocessors, low-power technologies, emulation, dynamic binary translation, performance analysis and optimisation.

(Jun 2009 — Mar 2011) Sofware Engineer, IBM

Cross-platform virtualization using binary translation, hardware support for dynamic optimisation, design and development of runtime dynamic optimizer.

(Jul 2007 — Jun 2009) Software Engineer, Transitive

Cross-platform virtualization using dynamic binary translation. Performance analysis and optimisation.

(Jul 2005 — Jul 2006) Intern Software Engineer, Oracle

Datacenter automation and failure recovery.