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.
-
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
-
Verified Dynamic Programming with Σ-types in Lean
Solving a competitive programming problem and proving it correct with dependent types
