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 users who like the study of programming languages, formal semantics, types, or linguistics.