I will collect here my notes & links to any talks that I give. Please let me know if anything is incorrect or unclear, or if you have any questions!
My thesis, on Geometric Perspectives on Program Synthesis and Semantics (October 2021). Abstract:
We develop a formalism to apply Watanabe’s Singular Learning Theory to the problem of program synthesis. In our case, a program is a sequence of letters on the tape of a Turing Machine, which we associate to a singularity of an analytic function. The key invariant associated to a singularity in this context is the real log canonical threshold, and we introduce methods to compute this value from an ideal generated by polynomials. We provide a semantic interpretation of these singularities, which distinguishes distinct algorithms by viewing them as the limit of a learning process.
An informal appendix to the previous, on blowing-up and calculating RLCTs.
Notes on Girard's strong normalisation theorem for System F (polymorphic lambda-calculus). Also includes some discussion of the relationship to Gödel's incompleteness theorems and second-order Peano arithmetic, expanding on some fairly cryptic remarks in Proofs and Types. (September 2020.) I gave a talk to the Computation, Geometry, Logic seminar based on these notes (July 2021, video lost to lockdown restrictions).
A poster and paper, on a partially observed model of invasive species control, published by Methods in Ecology and Evolution. Work conducted at the Melbourne Centre for Data Science. (July 2023, supplementary material.)
A short note on lattice paths in Young diagrams. I provide a (seemingly novel) bijective proof of an identity due to Carlitz, Roselle & Scoville, and answer explicitly an unsolved question raised in Stanley's Enumerative Combinatorics.
For practice and my own benefit, I am working on translating some papers from French, which I will collect here.
JP Serre's Géométrie algébrique et géométrie analytique (GAGA, to his friends). I have, currently at least, skipped some of the applications for which I didn't have the necessary background. (November 2021.)
"Inside every proof theorist is a sleeping bureaucrat." Jean-Yves Girard's From why to how: proof theory since 1950. Come for the insights, stay for the snarky footnotes. (December 2021.)