A Productive Week
This was a productive week. Since Wednesday, I've spent a significant amount of time revising some shoddy proofs I'd written back last summer, and managed to double-check them, fix some flaws, and even streamline them a bit. They feel like they might almost be correct!
For those who don't work with me directly, the proofs are concerning a calculus that clarifies the semantics of the client and server annotations that Links supports, which allow you to move your code from one to the other effortlessly, and ensure that it only runs in the appropriate place (if you care). I'm not sure whether this system has any broader impact than for explicating Links, but it's been a very educational experience for me trying to build it. Keep an eye out for it to be published sometime in the 2007–2010 timeframe.