Andrew K. Hirsch @akhirsch@types.pl
- website
- http://akhirsch.science
Postdoc at the Max Planck Institute for Software Systems. Types, security, and categories.
Joined Oct 2020
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?
- website
- http://akhirsch.science
Postdoc at the Max Planck Institute for Software Systems. Types, security, and categories.
Joined Oct 2020
