But then I'd have to come up with (at least partial) decision procedures, which sounds hard....

Show thread

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?

types.pl

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