Postdoc at the Max Planck Institute for Software Systems. Types, security, and categories.
But then I'd have to come up with (at least partial) decision procedures, which sounds hard....
Ugh, Coq keeps crashing on me. Apparently this proof just has too many goals. Not sure what to do about this... perhaps it's time to learn proof-by-reflection?
A Mastodon instance for programming language theorists and mathematicians. Or just anyone who wants to hang out.