December 8th, 2010

Quals countdown: T-8 days

I might not be doomed:

  • As of today, I'm finally caught up on TaPL -- that is, I have no more chapters left to read than I have days left to read them in. (Insert step-indexing joke here. Um.) I've been mostly skimming over the short implementation chapters, and I skipped the stuff about coercion semantics for subtyping and most of Chapter 21, which explains the metatheory of recursive types using coinduction, but other than that, I'm still on track to read the whole thing.
  • I checked with Dan about exactly how much of Davey and Priestley he expects me to actually absorb. It turns out that he'll be happy if I can explain Knaster-Tarski. I, too, will be happy if I can do that.
  • I read the first half of the Appel and McAllester "Indexed Model" paper. It makes so much more sense now than when I first tried to read it a year ago. Maybe indexed models of recursive types (as opposed to, for instance, the chapter of TaPL that I skipped) are both easier for human beings to understand and easier to mechanize from scratch! (They're not necessarily pretty, though. People use words like "infect" to describe what indices do to a model.)
  • It's starting to become clear (well, less opaque, anyway) how all of these things are related.

Slides from my "Theorems for low, low prices!" talk

I put up the slides from a talk I gave in B629 last week that sketched out the dynamic sealing project I've been working on with Amal Ahmed and Jacob Matthews. A paper is on the way (it'll be a revised, expanded, and improved version of their 2008 ESOP paper), but it's not fit for human consumption just yet.1

There's a lot to do still, but I've been working on this project off and on for almost a year, so it's very exciting to get to the point where I'm capable of giving a talk! Sadly, I ran short of time during the talk and wasn't able to show slide 18 (page 20 of the PDF), which is obviously the greatest slide ever.


  1. We had no problem subjecting my classmates to it, however.