Just a few things today.

1. I finally set up automatic nightly backups for the speeddating site. Cron is really a cool tool, I have to say, though I also have to say the interface kinda blows. It's really magical the first time you get an email from cron telling you about successful completion of some job you'd forgotten you scheduled. Pretty neat.


2. After that I dug up a bunch of the multi-language semantics stuff, brought it up-to-date with the new version of Redex, and got a simply-typed lambda-calculus embedded in an untyped-lambda calculus system working. That system, as it turns out, is pretty cool: you actually end up getting higher-order contracts in the Findler and Felleisen sense for free out of the embedding. After I'm done demonstrating that result a bit more formally, I'm going to show that embedding simply-typed lambda calculus onto itself can actually give you a language that's not strictly normalizing. Then there's a couple proofs, and then the big task of modelling and then proving correct a large system. This research is turning awesome everywhere I'm looking. Yay.


3. I read up on Reynold's separation logic for the PL reading group meeting. Nobody really understood the paper very well, but it seems very interesting nonetheless. We're reading about it again next time.


4. And some other stuff not really to be shared.