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.

PhD Thesis

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.

News and Media

27 Aug 2021

Upcoming talk on combinatorics and spined categories at Category Theory 2021, 3 Sep 2021, Genoa, Italy. (Joint work, presented by Ben Bumpus).

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!

05 May 2021

Prof. Gernot Heiser's blog post on our seL4 verification work hit the front page of news aggregator news.ycombinator.com today!

05 May 2021

My work on Translation Validation of the seL4 kernel was featured on the HENSOLDT Cyber GmbH website. Read the full article, including my comments, in English🇦🇺 and German🇩🇪!

26 Apr 2021

I gave a talk about degree of satisfiability at the CSIRO Trustworthy Systems seminar, including announcing some results on degree of satisfiability in Heyting Algebras.

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.

Contact

If you have any questions, or if you wish to hire me as a consultant, use the email address below. You can also find me on the Mathematics Stack Exchange and on Semantic Scholar.

To find out my email address, enter the number ---- below: