Future Blog Post
Published:
This post will show up by default. To disable scheduling of future posts, edit config.yml and set future: false.
Blog posts
2199
2025
Tutorial : A Verified Interpreter with Side Effects
Published:
1. Introduction
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 🐔
2015
Blog Post number 4
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
2014
Blog Post number 3
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
2013
Blog Post number 2
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.
2012
Blog Post number 1
Published:
This is a sample blog post. Lorem ipsum I can’t remember the rest of lorem ipsum and don’t have an internet connection right now. Testing testing testing this blog post. Blog posts are cool.