My interests are in functional programming, logic, type theory, and category theory. I enjoy writing code in Haskell, Agda, and Lean.

I spend most of time split between refining my course materials and adding to my digital library of mathematics. However, I make other projects available on here too.

• Digital library of formalised mathematics 📚 written in Lean.
• Lambda calculus computer 🧮 written in Haskell.
• Turing machine interpreter 🚂 written in Python.
• Course materials on the Curry-Howard isomorphism 📔
• Advent of Code 🎄🎅

I am a mathematics teacher in Christchurch, New Zealand. I am primarily involved with teaching first year undergraduates, but I do teach a second year class about logic and computation. I studied mathematics at the University of Canterbury (BSc Hons) and Australian National Univeristy (PhD) primarily studying algebraic geometry, algebraic number theory, and category theory. I wrote my thesis about Grothendieck's Galois Theory of schemes over the natural numbers. My interests have moved towards type theory, in particular as a language to express mathematics.