http://www.meetup.com/Bay-Area-Categories-And-Types/events/174846952/Slides not published yet
In short, pretty neat formalization of "always", "until", "since" in logic. Via fixpoints.
The problem is, I asked Valeria whether it can be equivalently interpreted in a Grothendieck topos over, say, ℕ; she said, well, it's like using cannons against flies.
But for me, it's rather way more natural than having pervert sex with alternative quantifiers.
Anyways, I probably have to prepare a series of talks on topos logic. No big deal actually.
But so far, next time Valeria will be talking on S4.