Blog

🛠️ This blog is under construction

Free Monads in Lean — A Four Part Series

Strictly positive thoughts on free monads in Lean for the mathematically inclined programmer

1. Part 1 – Defining the Free Monad in Lean
2. Part 2 – Catamorphisms, Interpreters, and Initial Algebras
3. Part 3 – Universal Morphisms and Effect Handlers
4. Part 4 – Tutorial: A Verified Interpreter with Side Effects

Verified Dynamic Programming with Σ-types in Lean

Solving a competitive programming problem and proving it correct with a novel use of dependent types - a beginner friendly tutorial

Coming Soon

Introduction to Computability Theory in Lean

Formalizing the theory of oracles and Turing degrees in a multi-part series exploring recursive functions, decidability, and the arithmetic hierarchy

Linear Logic: Syntax, Semantics and Applications

An introduction to the syntax and semantics of linear logic. We’ll explore its use in programming by looking at Par, a new process language implemented in Rust based on classical linear logic

LiHKAL (Logics I Have Known and Loved)

On the Varieties of Formal Systems