Fault-tolerant compilation
How do we implement logic on encoded qubits?
This is the question that underlies my whole programme: how does one compile a logical program onto a quantum error-correcting code and guarantee that it still works?
Quantum Group · University of Oxford
Research Associate in Quantum Software
I work on the mathematical foundations of fault-tolerance which are needed to compile computations into reliable error-corrected implementations on quantum computers.
I am a Research Associate in Quantum Software in the Quantum Group at the University of Oxford. My research is about the mathematical foundations of quantum computing: I have worked on diagrammatic reasoning, measurement-based quantum computation, measures of non-classicality, and quantum computation with continuous variables.
The problem that most excites me at the moment is fault-tolerant quantum compilation: any useful quantum computation will have to run on error-corrected, logical qubits, and we still lack the mathematical tools to compile programs onto them systematically across different codes and architectures, with guarantees that the result is still correct. I attack this with the tools I know best: algebra (especially symplectic and stabiliser structure), category theory, graphical calculi, and the design and semantics of programming languages.
Academic path
Quantum computers will only ever be useful if they are fault-tolerant: computations must run on logical qubits, encoded in error-correcting codes, using operations that keep errors under control. Compiling a program down to this level is requires very different techniques from ordinary compilation: the physical implementation must be carefully orchestrated so that errors are caught whenever they occur. My research builds the mathematical foundation on which such a compiler can be designed: algebraic structures that describe codes and logical operations compositionally, graphical calculi to reason and compute with them, and semantics that say precisely what a quantum program means and what structure needs to be preserved during compilation.
How do we implement logic on encoded qubits?
This is the question that underlies my whole programme: how does one compile a logical program onto a quantum error-correcting code and guarantee that it still works?
What is the right algebra for quantum computation, and can we reason about it diagrammatically?
Graphical languages turn quantum-mechanical reasoning into diagram rewriting, and are natural intermediate representations for program synthesis and optimisation.
What does a quantum program mean, and how do its pieces compose?
Trusthworthy compilation a precise, compositional account of what programs mean. Semantics provides this formal grounding and makes compilation into something you can verify.
How do we reason about infinite-dimensional quantum systems?
Bosonic systems are infinite-dimensional in which computation, non-classicality, and error correction all make sense. Hardware is being designed around these computational models, but the theoretical tools to reason about them are nowhere near as developped as for qubits.
Earlier work: My PhD extended measurement-based quantum computation beyond qubits and before that I worked on experimental quantum thermodynamics and metrology in Rome.
Long term: these threads converge on a single algebraic framework for fault-tolerant compilation: one in which logical operations on any code can be described, synthesised, optimised, and formally verified, with quantitative guarantees on how errors propagate.
Nothing matches —
Peer-reviewed
What stabiliser quantum programs mean, compositionally.
A graphical calculus built on symplectic structure, spanning stabiliser and Gaussian quantum mechanics.
Finite effective descriptions capture everything operationally accessible about bosonic systems.
When continuous-variable measurement patterns define deterministic computations.
A toolkit of results for qudit stabiliser ZX-calculus in odd prime dimensions.
Generalising flow-based determinism to qudit measurement-based computation.
Two central notions of quantumness coincide in the continuous-variable setting.
Complete equational theories for qudit stabiliser quantum mechanics.
Preprints
The compositional structure of quantum operations with classical input and output.
Concrete semantics for recursive hybrid quantum–classical programs.
Generalised surgery implementing entangling logical gates between arbitrary CSS codes.
A complete graphical calculus for the Gaussian, continuous-variable world.
Also on Google Scholar · ORCiD · arXiv.
Nothing matches —
If you would like me to speak at your seminar or event, get in touch.
Categories and Quantum Informatics — lectures, computer labs, and course material, University of Edinburgh (2023). This work earned a University of Edinburgh Staff Award.
Introduction to Quantum Programming and Semantics — guest lectures and tutorials, University of Edinburgh (2024).
I have served on the programme committees of QPL, ACT, and PLanQC, review for Quantum, Compositionality, and LMCS among others, and organised the Quantum Software Lab seminar in Edinburgh (2023–2025).
Students supervised
I welcome students interested in the algebra of quantum computing, fault tolerance, or quantum programming languages — feel free to reach out.
Robert I. Booth
Quantum Group
Department of Computer Science
University of Oxford
Elsewhere