Every now and then, I cave in and look at the Reddit comments on my blog posts. Recently, someone wanted to know the difference between “inflationary” and “monotonic” functions. I’m glad you asked!
I’m going to be on stage a couple of times at the SPLASH conference this October in Pittsburgh. If you’ll be there, please say hello!
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.
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.