The American Mathematical Society wrote a memorial notice on Vladimir Voevodsky where, among others, his contributions to type theory are considered.
If you’re a programmer and you want to understand what is homotopy type theory about, Dan Licata has a talk on the topic.
Interactive theorem proving such as one provided by Agda is so empowering. The help provided by the compiler while interactively developing a proof is invaluable. Types guide you to a solution at every single step.
After an interruption today, my web page is back online.
If you ever wondered how are types different from sets or more generally what is the difference between type theory and set theory, I recommend watching a talk by Thorsten Altenkirch at Foundations of Mathematics: Univalent Foundations and Set Theory 2016.
I applied to give a theorem proving seminar at a university. They chose Philip Wadler as a lecturer over me. That must have been close! Still, so disappointed…
Isn’t it ironic – Google’s own proprietary Meet service isn’t supported in Chromium, a web browser by Google, but it is supported in Firefox, a web browser by Google’s competitor.
Jo Freeman has an interesting essay on the tyranny of structurelessness. The lack of structure implies the lack of power to act.
I’m happy to announce that I’ll be speaking at the Lambda Days 2019 conference! I’ll be giving a talk on function totality.