Comment by steego

Great notes!

I think it’s also worth noting that Barry Jay has a particularly strong vantage point for unearthing this particular foundational candidate. First, his advisor was Joachim Lambek, who’s responsible for adding Category Theory in the Curry-Howard-Lambek correspondence.

If one looks at Barry’s body of work over his lifetime, it’s no surprise it would culminate into an elegantly beautiful system capable of self-reflection.

I think his 2025 PEPM paper did a great job explaining the ideas to a regular programmer / wannabe academic like myself: https://github.com/barry-jay-personal/typed_tree_calculus/bl...