• Foundations of Algorithmic Randomness and Computability

  An introduction to computability theory, turing degrees, and randomness, supported by a Lean formalization

  34 min read   ·   February 07, 2026

  2026   ·   computability   randomness   lean   formal-verification   kolmogorov-complexity   ·   Computability   Randomness

• 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