Log

Last updated: 18/05/2023.

Ongoing

maintainer of the Vampire automatic theorem prover

2023

program committee for the 25^th International Symposium on Symbolic and Numeric Algorithms for Scientific Computing
invited talk Takin’ Off: Deploying Neural Models for Theorem Proving at the Joint EuroProofNet Workshops on Practical Aspects of Machine Learning in Theorem Proving and Dataset Generation for Data-Deficient Domains (JEPNWPAMLTPDGD³)
preprint Lemmas: Generation, Selection, Application
co-chair of 14^th International Workshop on the Implementation of Logics (IWIL), co-located with LPAR-24
organising the 7^th Vampire workshop
program committee for the 8^th Conference on Artificial Intelligence and Theorem Proving (AITP)
program committee for TABLEAUX 2023
committee for the 7^th edition of the VCLA International Student awards

2022

preprint Linear Refutation and Clause Splitting
delivered the formal methods MSc seminar
invited talk Machine Learning for Theorem Proving: What I Wish I Had Known 5 Years Ago at the 7^th Conference on Artificial Intelligence and Theorem Proving (AITP)
published The Rapid Software Verification Framework at FMCAD 2022
published Automating Security Analysis of Off-Chain Protocols at FMBC 2022
published Reuse of Introduced Symbols in Automatic Theorem Provers and The Vampire Approach to Induction at PAAR 2022
program committee for the 7^th Conference on Artificial Intelligence and Theorem Proving (AITP)

2021

talk Learning From Subgoals at the formal methods workshop of Eszterházy Károly Catholic University
new position at TU Wien, Austria with Laura Kovács, working on the ERC project ARTIST
published On Evaluating Theorem Provers at the Third International ARCADE (Automated Reasoning: Challenges, Applications, Directions, Exemplary Achievements) Workshop
published A Multithreaded Vampire with Shared Persistent Grounding at FMCAD 2021
program committee for the workshop on Parallel and Distributed Automated Reasoning 2021
published Eliminating Models during Model Elimination at TABLEAUX 2021

2020

In 2020 I took a position with Giles Reger working on the EPSRC project CAPS: Collaborative Architectures for Proof Search.

PhD

From 2017 to 2020 I was a PhD student in the school of Computer Science, University of Manchester. My thesis was on Applications of Machine Learning to Automated Reasoning, supervised by Giles Reger and Andrei Voronkov. You might be looking for material from that time, which includes

BA

Before that, I read Computer Science (with Physics!) at the Computer Laboratory, University of Cambridge. My Part II dissertation was entitled Verified Metatheory and Type Inference for a Name-Carrying Simply-Typed λ-Calculus, supervised by Dominic Mulligan and Victor Gomes. It has a corresponding entry in the Isabelle Archive of Formal Proofs.