This post will be a relatively short note on a simple self-interpreter for the lambda calculus I recently made. I’ve been thinking of making an extensive work, perhaps a book, on programming in the lambda calculus. As part of that, I was looking into self-interpretation. If one wants to do... [Read More]

Approximating Digital Functions Iteration Sums Products A Quadratic Product Recursive Types and Recursion Quicksort, First Pass Defunctionalization Final Quicksort Final Thoughts [Read More]

ℕ ≅ ℕ × ℕ ℕ ≅ ℕ + ℕ Initial Algebras Initial Algebras Extras Lambda Expressions Peano Expressions Sorted Trees Trees of Bounded Height Final Thoughts [Read More]

A few years ago, a new proof theory called CaTT was described in the paper A Type-Theoretical Definition of Weak ω-Categories [Read More]

This post will be a small note on program specifications. One of my long-term goals is that of a bootstrapping program synthesizer. That is, a program synthesizer that can synthesize better program synthesizers. One important step is specifying, formally, what this means. I’ve recently figured out how to properly formulate... [Read More]