• The Free Monad: A Four-Part Series

  A four-part series on free monads in Lean

  2 min read   ·   May 21, 2025

  2025   ·   lean   free-monads   category-theory   effects   ·   Formal-Verification   Free-Monads

• Verified Dynamic Programming with Σ-types in Lean

  Solving a competitive programming problem and proving it correct with dependent types

  20 min read   ·   May 21, 2025

  2025   ·   lean   dynamic-programming   formal-verification   dependent-types   sigma-types   ·   Formal-Verification   Algorithms

---

Coming Soon

Introduction to the ZX-calculus

A diagrammatic language for expressing and reasoning about quantum processes via monoidal categories

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

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