Blog

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

The Free-er Monad

Strictly positive thoughts on freer monads in Lean for the mathematically inclined progammer

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.