How to learn to do determinism proofs

A couple days ago, my advisor asked me what reading material I would suggest to a new student who wants to learn to do determinism proofs like the ones we did for LVar calculi. This is a good question! Even assuming that one knows what one means by “determinism”, I think it’s hard to come by good introductory examples of determinism proofs. If you want to know (or refresh your memory on) how, say, a standard progress-and-preservation type safety proof is set up, you can flip to chapter 8 of TAPL. But I don’t know of a similar standard resource for how a proof of determinism is set up.

A month of daily check-ins

Some time ago, in response to my asking what I should write about on this blog, Sumana suggested I write about what my typical day is like. I demurred, saying that there was no typical day. For the last month and change, though, I’ve been doing an exercise in which, each day that I’m at work, I take some notes about what I did on the previous work day and what I plan to do that day. So, here’s a month (plus a few days) of daily check-ins, and you can conclude for yourself whether there’s such a thing as a “typical” day.

Embedding, deep and shallow

Not long ago, I wanted to better understand the notions of “deeply” and “shallowly” embedded languages. Here I mean “embedded” in the sense of, say, “domain-specific language embedded in Haskell”, although it doesn’t actually matter to me what the host language is, or whether the embedded language is “domain-specific”.

Call for papers: IFL 2015

Once again this year, I’m serving on the program committee for IFL, the annual Symposium on Implementation and Application of Functional Languages, and the call for papers is open. This year’s symposium will be in Koblenz, Germany, over September 14-16. If you’re in Europe and ICFP’s just a bit too far away for you to justify going this year, IFL is a nice substitute!