Blog

🛠️ This blog is under construction, but here are the upcoming posts:

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

Introduction to Computability Theory in Lean (Part 1)

Formalizing the theory of oracles and Turing degrees

ZkFlow: A Formally Verified Compiler for Zero-Knowledge Circuits

From declarative syntax to ZK constraints - verified in Lean

Chicken-pi: A Toy Proof Assistant in Haskell

A Coq-inspired toy proof assistant with inductives, dependent types, pattern matching, and universes — baked in Haskell.