I work in the Trustworthy Systems Research Group of CSIRO, Australia's national science research agency. I use techniques from mathematical logic to help create trustworthy software and hardware that comes with strong security, safety and reliability guarantees.
I obtained my PhD in Mathematics at the University of Manchester in October 2019, under the supervision of Prof. Alexandre Borovik. My PhD thesis explored algebraic applications of Internal Set Theory, an axiomatic set theory developed by Edward Nelson as a foundation for Nonstandard Analysis. Highlights from my thesis include a powerful extension theorem for actions of LEF groups on compact manifolds, along with a "Robinsonian" characterization theorem for sheaves on topological spaces. Introducing a non-standard extension of Martin-Löf Type Theory allowed me to formally verify the main results of my thesis using the Agda interactive theorem prover. I also made some contributions to the theory of degrees of satisfiability in probabilistic group theory, and to the theory and practice of stochastic optimization in computer science. I have 16 refereed publications in international journals and conferences (listed in my CV). Click the buttons below to find out more about my research interests!
Which one of these three point clouds can we get by sampling the unit cube using a pseudo-random sequence? Surprisingly, the answer is any one of them, depending on the sequence we use. We used three sequences to sample the same manifold: the unit cube, which has one connected component and no holes. However, the first two sequences fail to yield a uniform sample. In the first case (RANDU), the resulting point cloud seemingly consists of 15 separate connected components. In the second case (XorShift64, scaled), there is only one component, but it has many holes. Using persistent homology, one can rigorously define the Betti numbers of point samples, and investigate their relationship to the Betti numbers of the sampled manifold. In my honors thesis I classified some pseudorandom sequences based on their ability to reflect the topological properties of the manifolds they sample, and developed an algorithm that can test for failures of uniformity by calculating persistent homology groups of the samples..
Degree of Satisfiability
Which non-Abelian group is closest to being Abelian? Which composite number is farthest from being prime? Such questions can be formulated and answered using the theory of Degree of Satisfiability (and result in striking visual arrangements that feature heavily on this web page). The degree of satisfiability of a logical formula φ(x,y) is the probability that φ(a,b) holds for uniformly randomly chosen a,b. A famous theorem of Gustafson states that the degree of satisfiability of the equality xy=yx is at most 5/8 in a non-Abelian group, with equality obtained in the Quaternion Group. Hence, one can say that the Quaternion Group is closest to being Abelian among all the non-Abelian groups. The degree of satisfiability of equations in infinite groups gives significant information about algebraic structure, e.g. about virtual properties. I proved results about the degree of satisfiability of some special equations, and introduced criteria to identify which equations hold in a finite index subgroup precisely if they have positive degree of satisfiability.
My PhD thesis (available here) explores two novel algebraic applications of Internal Set Theory. I prove that every profinite group admits a finite approximation in the sense of Zilber, and my main result shows that well-behaved actions of the approximating group on a compact manifold give rise to similarly well-behaved actions of periodic subgroups of the approximated group on the same manifold. This generalizes earlier results of Manevitz and Weinberger on circle actions to a large class of groups. Motivated by the extraction of computational bounds from proofs in a pure fragment of IST, I devised a pure presentation of sheaves over topological spaces in the style of Robinson and proved it equivalent to the usual definition over standard objects. By introducing a non-standard extension of Martin-Löf Type Theory I formally verified my results using the Agda proof assistant.
I received the CSIRO SCS Engineering and Technology Award, awarded for our high-impact work on binary verification for the 64-bit RISC-V architecture (along with my teammates Matthew Brecknell and Dr Mitchell Buckley).
06 May 2021
Click here to read the RISC-V International coverage of my work, bringing Translation Validation to RISC-V!
I find the Big City and the Great Outdoors equally comfortable. On my day off, you're just as likely to meet me in the dense urban area of the Sydney CBD as in the coastal bushlands of New South Wales.
If you live in the UK, you may know me from Manchester Orators, a chartered club for the promotion of public speaking, presentation and leadership skills. I was a member between 2017 and 2019, and I hope to return one day.
At home, you'll find me in the kitchen. Fusion cuisine, simple ingredients, mise en place. Sometimes, something good comes out of it.