Holbert 0.5 is now live on liamoc.net/holbert.

It now supports inductive judgements, induction and rule inversion, better unification solutions, many bug fixes, better rewriting support, and many other small improvements. This is mostly due to the great work from my two undergrads over the last year, Chris Perceval-Maxwell and Rayhana Amjad.

If you see an error message on load, you may have to clear your cache.

Hello everyone. I probably will not post significantly here for now, but I am parking the profile in case it becomes more widely used.


A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.