Lots of little things today. I actually didn't end up doing that much, but I got little pieces of lots of things to happen.

The morning was essentially for the programming contest spec. Another draft out the door, more revisions, et cetera. I also spent a good chunk of the afternoon doing the same thing. It's surprising in a technical specification how difficult it is to make everything work out, how many tiny things there are that have to be right or else the document doesn't work. Makes it a big pain to get these things right.

Also today the guy who maintains the PLT Scheme web pages did a new revision of the code that generates HTML. Since I control the PLaneT page, that means I need to propagate the updates there.

After I found out about that, I started up on the declarative images and 3D anaglyphs paper I was talking about yesterday. After about a paragraph and a half, I ran into Robby and he said he thought it'd be better to scrap the whole thing to focus more on the foreign interface semantics. I'm kind of glad of that, actually. I tend to sign myself up for too much, and while this wasn't a lot it isn't like I have nothing to do.

So when that was done I worked on the multilanguage semantics stuff. Robby thought that the right way to represent the dynamic checks you need to guarantee type soundness was as guard functions that get distributed just like contracts. I worked that out, and actually I'm not sure that works well -- the thing is, exactly what needs to be checked, if anything, depends on the reason the conversion is being performed, and that information isn't known if you separate the dynamic checking out from the conversion process ... I think. On the other hand, having the dynamic check separate from the translation is useful to a major theorem I want to prove, so I did a version where the mapping functions introduce guards but those guards are represented separately. The guards don't distribute, though: they're just straight up projections. Probably you could show that guard composed with translate composed with translate back is a retract or something, I dunno, sounds plausible. We'll see.

In other news, I'm a big nerd. I got my tax refund and decided to spend it on a few expensive computer books I've wanted for a long time. So now, coming to my office courtesy of Amazon: The Lambda Calculus, one of the few books important enough to be known by the last name of its author, Essentials of Programming Languages, and Lisp in Small Pieces. I've wanted all of these books for a long time, so I'm glad to be getting them. Thanks Uncle Sam!