The call for submissions for Off the Beaten Track 2015 is open, and I’m very excited and proud to be serving on the program committee this year!
One of the ideas that has been important to me as I’ve worked on LVars is the notion of a frame property. A frame property captures the idea of local reasoning about programs that alter state. Written as an inference rule (where the truth of the stuff above the line allows us to infer the truth of the stuff below), it might look something like this frame rule, due to O’Hearn, Reynolds, and Yang from their work on separation logic:
Inspired by Brent Yorgey, I’m finally going public with a draft of my dissertation!
My thesis is that a certain kind of data structures, which I call “lattice-based data structures” or “LVars” for short, lend themselves well to guaranteed-deterministic parallel programming. My dissertation combines material from various previously published papers, making it a three-papers-stapled-together dissertation in some sense, but I’m also retconning a lot of my work to make it tell the story I want to tell now.
When people ask what the best introduction to LVars is, I have trouble recommending the first LVars paper; even though it was only published a year ago, my thinking has changed quite a lot as my collaborators and I have figured things out since then, and the paper doesn’t match the way I like to present things now. So I’m hoping that my dissertation will be something I can point to as the definitive introduction to LVars.1 I’m also generalizing some of our previously published results, now that we know that that’s possible.