Sitemap
A list of all the posts and pages found on the site. For you robots out there is an XML version available for digesting as well.
Pages
Posts
Tutorial : A Verified Interpreter with Side Effects
Published:
1. Introduction
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 🐔
portfolio
Portfolio item number 1
Short description of portfolio item number 1
Portfolio item number 2
Short description of portfolio item number 2
publications
Paper Title Number 1
Published in Journal 1, 2009
This paper is about the number 1. The number 2 is left for future work.
Recommended citation: Your Name, You. (2009). "Paper Title Number 1." Journal 1. 1(1).
Download Paper | Download Slides
Paper Title Number 2
Published in Journal 1, 2010
This paper is about the number 2. The number 3 is left for future work.
Recommended citation: Your Name, You. (2010). "Paper Title Number 2." Journal 1. 1(2).
Download Paper | Download Slides
Paper Title Number 3
Published in Journal 1, 2015
This paper is about the number 3. The number 4 is left for future work.
Recommended citation: Your Name, You. (2015). "Paper Title Number 3." Journal 1. 1(3).
Download Paper | Download Slides
Paper Title Number 4
Published in GitHub Journal of Bugs, 2024
This paper is about fixing template issue #693.
Recommended citation: Your Name, You. (2024). "Paper Title Number 3." GitHub Journal of Bugs. 1(3).
Download Paper
talks
Talk 1 on Relevant Topic in Your Field
Published:
This is a description of your talk, which is a markdown file that can be all markdown-ified like any other post. Yay markdown!
Conference Proceeding talk 3 on Relevant Topic in Your Field
Published:
This is a description of your conference proceedings talk, note the different field in type. You can put anything in this field.
teaching
Teaching experience 1
Undergraduate course, University 1, Department, 2014
This is a description of a teaching experience. You can use markdown like any other post.
Teaching experience 2
Workshop, University 1, Department, 2015
This is a description of a teaching experience. You can use markdown like any other post.