Tutorial : A Verified Interpreter with Side Effects
Published:
Blog posts
2025
Universal Morphisms and Effect Handlers
Published:
1. Introduction
As we recall from part 1, free objects are defined by left adjoints to forgetful functors, and can also be defined by a particular universal property. Universal properties are given by universal arrows: unique morphisms that characterize an object up to isomorphism. In part 2, we talked about one particular universal property, and this part will focus on another.
Initial Algebras, Catamorphisms, and Interpreters
Published:
In the last section, we introduced the free monad and implemented it in Lean. In this section we will study the theory a bit more deeply, by understanding the notions of algebra and universality.
Part 1: Defining the Free Monad in Lean
Published:
1. Introduction
ZkFlow: A Formally Verified Compiler for Zero-Knowledge Circuits
Published:
🚧 Under construction 🔐
Verified Dynamic Programming with Σ-types in Lean
Published:
1. Introduction
If you’ve taken an algorithms class, you have likely seen dynamic programming, specifically a technique called memoization. Memoization works to optimize recursive algorithms by caching the solutions to subproblems in a table, and when a subproblem is encountered, it queries the table instead of recomputing the solution. This gives us an exponential performance boost.
The Free-er Monad
Published:
Free monads provide a way to represent effectful sequential programs as pure syntactic data, separate from their interpretation. You describe what should happen as an abstract tree of effects, leaving open how you want it to happen. By decoupling syntax from semantics like this you gain full control over how programs are evaluated and interpreted - for example we could interpret a syntax tree in multiple ways:
Introduction to Computability Theory in Lean (Part 1)
Published:
🚧 Under construction
Chicken-pi: A Toy Proof Assistant in Haskell
Published:
🚧 Under construction 🐔