I like to write about things I spend time thinking about or working on, and lately that tends to land on the algebraic and categorical foundations of functional programming, as well as logic and formal methods more broadly.
-
Quantum Algorithms in Lean
Formalizing and verifying textbook quantum algorithms in the query-combinator model
-
Currying in Categories
Cartesian closed categories and the Curry-Howard correspondence
-
Partiality in a Total Type Theory ▸ 3 parts
Modeling divergence and nontermination in Lean
-
Foundations of Algorithmic Randomness and Computability
An introduction to computability theory, Turing degrees, and randomness
-
The Free Monad ▸ 3 parts
A three-part series on free monads in Lean
