I've been ridiculously busy the last few months, so this is just a quick link:

John retired recently, so I should probably post something in his honor. When I have time, I'll post a little something about some of John's work (with Peter O'Hearn) on how to use functor-category semantics as a guide to programmming with polymorphism. If you don't want to wait, you can look at their paper

*From Idealized Algol to Polymorphic Linear Lambda Calculus*.