WAIT is the ObsTT + impredicativity paper out I need to read it

Forget hierarchy theories and McBride monads. Observational equality is where it's at

I still think it's funny they gave a name to the monad at all, let alone called it after someone
Completely unnecessary, it's great

Sign in to participate in the conversation

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