I've previously blogged about the principles of constructive provability logic and about our paper on the topic being accepted to IMLA. Since then (in fact, since my last blog post), I've given three versions of a talk on the logic: first at CMU before I left for my internship at Microsoft Research, the second at the workshop on Intuitionistic Modal Logic and Applications in Nancy, France,1 and the third the next day at LIX in Saclay (south of Paris) France.2 After tweaking that talk three times, I decided to tweak it once more and put it on the web on my page of resources about Constructive Provability Logic.
This was actually quite a bit harder than I'd expected! It didn't seem quite as difficult when I did it for the Linear Logical Algorithms presentation a few years ago, but I guess I was forcing myself to be less perfectionist there (requiring one take instead of 4 definitely forces you to be less perfectionist). Especially in the first two videos, the number of repeated takes comes across in my rather affected tone of voice - which is what you get when you over-rehearse something, at least if "you" is a person who (like me) has forgotten anything he ever learned about the "illusion of the first time".
The effort required was such that I don't realistically see myself doing this too often again, but hopefully this will be at least moderately helpful to someone.
1 While in Nancy, I took a picture out of the window of the dorm where I was staying, and thereby whittled away a few more of my 15 minutes of fame.
2 Nothing famous happened there, but I did have excellent fondue.
SIGBOVIK 2017: ABC
3 weeks ago