Tree Calculus is an alternative to lambda calculus that is capable of doing meta-theory without having to construct or bolt on something else entirely.
If lambda calculus provides a theoretical foundation for a language like Lisp. Tree calculus provides a theoretical foundation for a Lisp with a macro system that is fundamentally part of the core calculus.
You don’t have to write parsers and other stuff to do meta programming. It’s fundamentally built in and the paper I posted above explores how to construct type systems as a library, not as something that is outside of the runtime environment.
Here’s what’s really cool about it too: Just like lambda calculus, you can evaluate tree calculus with pencil and paper.
My friend this ain't memes or celebrity news, it's theoretical computer science. You'll get out of it roughly what you're ready to put into it. If you're short on time, the grammar is like 5 characters and the proof of the halting problem isn't much bigger. If you don't already know why that is interesting though you really might have to read a bit to find out
That's my complaint, this page is essentially a meme.
And yes, i know enough about computer science to know that making an axinomic system with a short grammar that has a proof that the halting problem is undecidable, isn't particularly note worthy by itself. I highly doubt the reason people are interested in this is just code golfing a proof of the undecidability of the halting problem