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?


A Mastodon instance for users who like the study of programming languages, formal semantics, types, or linguistics.