My interests are in functional programming, logic, type theory, and category theory. I enjoy writing code in Racket, 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.