Anthony Hart

About a year ago, I had an idea for a relational programming language.

About four months ago, my dad came to my home with a dog in tow.

I’ve talked a lot about pairing functions on this blog.

In an earlier post, I mentioned a potential project where I’d talk about, among other things, logic programming within the lambda calculus a la MiniKanren.

My viewpoint on calculus, specifically differentiation, has changed rather radically recently.

This post will be a relatively short note on a simple self-interpreter for the lambda calculus I recently made.

Approximating Digital Functions Iteration Sums Products A Quadratic Product Recursive Types and Recursion Quicksort, First Pass Defunctionalization Final Quicksort Final Thoughts Introduction I’ve been a bit obsessed with continuous computation recently.

ℕ ≅ ℕ × ℕ ℕ ≅ ℕ + ℕ Initial Algebras Initial Algebras Extras Lambda Expressions Peano Expressions Sorted Trees Trees of Bounded Height Final Thoughts Introduction I’ve been researching methods for generating data the past few months and, as part of that, I

A few years ago, a new proof theory called CaTT was described in the paper A Type-Theoretical Definition of Weak ω-Categories It contains what is, in retrospect, the simplest and easiest to reason about presentation of ω-categories anywhere I’m aware of.…

This post will be a small note on program specifications.

Introduction Why Not Use Ordinary Compression?

I’ve known for a while that dependent types can be defined as initial and final dialgebras.

In this post, I will show a nice, clean, organized, schematic, and theoretically well-justified approach to sorting.

This post consists of some notes on lambda encodings I made a while ago.

I read a rather fascinating paper recently called “Implicative algebras: a new foundation for realizability and forcing”.